Miscellaneous style tweaks:

- fix four style linter warnings - use focusing dots more when there are multiple goals - remove a few superfluous dsimp only calls.
leanprover-community · Jul 7, 2024 · 5c52693 · 5c52693
1 parent b046eb6
commit 5c52693
Show file tree

Hide file tree

Showing 8 changed files with 8 additions and 19 deletions.
diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean
@@ -269,7 +269,7 @@ theorem ContDiff.uncurry_left' (n : ℕ∞) {f : E × F → G}
 theorem ContDiff.uncurry_left {f : E → F → G} (n : ℕ∞) (hf : ContDiff 𝕜 n ↿f) (x : E) :
     ContDiff 𝕜 n (f x) := by
   have : f x = (uncurry f) ∘ fun p : F ↦ (⟨x, p⟩ : E × F) := by ext; simp
-  rw [this] ; exact hf.comp (ContDiff.inr x n)
+  rw [this]; exact hf.comp (ContDiff.inr x n)
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
@@ -297,7 +297,7 @@ theorem Smooth.uncurry_left
     Smooth I' IP (f x) := by
   have : f x = (uncurry f) ∘ fun p : M' ↦ ⟨x, p⟩ := by ext; simp
   -- or just `apply hf.comp (Smooth.inr I I' x)`
-  rw [this] ; exact hf.comp (Smooth.inr I I' x)
+  rw [this]; exact hf.comp (Smooth.inr I I' x)
 
 end helper
 

diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean
@@ -278,7 +278,6 @@ theorem ChartPair.dist_update' [FiniteDimensional ℝ E'] {δ : M → ℝ} (hδ_
     simp only [OpenSmoothEmbedding.update_apply_embedding]
     dsimp only [ChartPair.mkHtpy]
     rw [dif_pos h𝓕, OpenSmoothEmbedding.updateFormalSol_apply]
-    dsimp only
     simp_rw [OpenSmoothEmbedding.update_apply_embedding, OneJetBundle.embedding_toFun,
       OpenSmoothEmbedding.transfer_proj_snd]
     rfl

diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
@@ -305,20 +305,18 @@ theorem oneJetBundle_chart_target (x₀ : J¹MM') :
   erw [hom_trivializationAt_target]
   simp only [trivializationAt_pullBack_baseSet, TangentBundle.trivializationAt_baseSet]
   rcases x₀ with ⟨⟨m, m'⟩, φ⟩
-  dsimp only
   simp only [ContMDiffMap.coe_fst, ContMDiffMap.fst_apply, ContMDiffMap.coe_snd,
     ContMDiffMap.snd_apply]
   erw [prod_univ, inter_eq_left, prod_univ, PartialEquiv.prod_symm, PartialEquiv.prod_symm]
   rw [preimage_preimage, ← Set.prod_eq, PartialEquiv.refl_symm, PartialEquiv.prod_coe,
       PartialEquiv.refl_coe]
-  dsimp only
   have : (fun x : ModelProd (ModelProd H H') (E →SL[σ] E') ↦ ((chartAt H m).toPartialEquiv.symm.prod (chartAt H' m').toPartialEquiv.symm) x.1) =
       (Prod.map (chartAt H m).symm (chartAt H' m').symm) ∘ Prod.fst := by
     ext x <;> rfl
   rw [this, preimage_comp, preimage_prod_map_prod]
   mono
-  exact (chartAt H m).target_subset_preimage_source
-  exact (chartAt H' m').target_subset_preimage_source
+  · exact (chartAt H m).target_subset_preimage_source
+  · exact (chartAt H' m').target_subset_preimage_source
 
 section Maps
 

diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean
@@ -95,7 +95,6 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
   erw [← preimage_vadd_neg, mem_preimage, mem_slice, R.mem_relativize]
   congr!
 
-
 theorem relativize_slice_eq_univ {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
     {p : DualPair <| TangentSpace (IP.prod I) σ.1.1}
     (hp : p.π.comp (ContinuousLinearMap.inr ℝ EP E) = 0) :
@@ -220,9 +219,7 @@ theorem FormalSol.eq_iff {F₁ F₂ : FormalSol R} {x : M} :
 theorem FamilyOneJetSec.isHolonomicAt_curry (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N)
     {t : N} {s : P} {x : M} (hS : (S t).IsHolonomicAt (s, x)) : (S.curry (t, s)).IsHolonomicAt x := by
   simp_rw [OneJetSec.IsHolonomicAt, (S.curry _).snd_eq, S.curry_ϕ] at hS ⊢
-  dsimp only
   rw [show (S.curry (t, s)).bs = fun x ↦ (S.curry (t, s)).bs x from rfl, funext (S.curry_bs _)]
-  dsimp only
   refine (mfderiv_comp x (S t).smooth_bs.mdifferentiableAt
     ((mdifferentiableAt_const I IP).prod_mk smooth_id.mdifferentiableAt)).trans
     ?_

diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean
@@ -568,7 +568,6 @@ theorem transfer_localize (hF : range (F.bs ∘ φ) ⊆ range ψ) (x : X) :
   · dsimp only; erw [ψ.right_inv (hF <| mem_range_self x), Function.comp_apply, F.bs_eq]
   · -- Porting note: was simp_rw [← ψ.fderiv_coe, continuous_linear_map.comp_apply,
     --  continuous_linear_equiv.coe_coe, continuous_linear_equiv.apply_symm_apply]
-    dsimp only
     -- Porting note: we are missing an ext lemma here.
     apply ContinuousLinearMap.ext_iff.2 (fun v ↦ ?_)
     erw [← ψ.fderiv_coe, ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe,

diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean
@@ -85,7 +85,6 @@ theorem IsHolonomicAt.congr {𝓕 𝓕' : JetSec E F} {x} (h : IsHolonomicAt
     IsHolonomicAt 𝓕' x := by
   have h'' : 𝓕.f =ᶠ[𝓝 x] 𝓕'.f := by
     apply h'.mono
-    dsimp only
     simp_rw [eq_iff]
     tauto
   unfold JetSec.IsHolonomicAt
@@ -104,7 +103,6 @@ theorem _root_.Filter.Eventually.isPartHolonomicAt_congr {𝓕 𝓕' : JetSec E
   intro x hx
   have hf : 𝓕.f =ᶠ[𝓝 x] 𝓕'.f := by
     apply hx.mono
-    dsimp only
     simp_rw [eq_iff]
     tauto
   unfold JetSec.IsPartHolonomicAt

diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean
@@ -149,9 +149,10 @@ theorem FamilyJetSec.uncurry_φ' (S : FamilyJetSec E F P) (p : P × E) :
 open ContinuousLinearMap
 theorem FamilyJetSec.uncurry_mem_relativize (S : FamilyJetSec E F P) {s : P} {x : E} :
     ((s, x), S.uncurry (s, x)) ∈ R.relativize P ↔ (x, S s x) ∈ R := by
-  rw [RelLoc.relativize, mem_preimage, oneJetSnd_eq, JetSec.coe_apply,  JetSec.coe_apply, S.uncurry_f, S.uncurry_φ']
-  dsimp only
-  suffices ((D (fun z ↦ f S z x) s).comp (fst ℝ P E) + (φ S s x).comp (snd ℝ P E)).comp (ContinuousLinearMap.inr ℝ P E) = JetSec.φ (S s) x by
+  rw [RelLoc.relativize, mem_preimage, oneJetSnd_eq, JetSec.coe_apply, JetSec.coe_apply,
+    S.uncurry_f, S.uncurry_φ']
+  suffices ((D (fun z ↦ f S z x) s).comp (fst ℝ P E) + (φ S s x).comp (snd ℝ P E)).comp
+      (ContinuousLinearMap.inr ℝ P E) = JetSec.φ (S s) x by
     rw [this]; rfl
   ext v
   simp_rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply,
@@ -216,7 +217,6 @@ theorem FamilyJetSec.isHolonomicAt_curry (S : FamilyJetSec (P × E) F G) {t : G}
     (hS : (S t).IsHolonomicAt (s, x)) : (S.curry (t, s)).IsHolonomicAt x := by
   simp_rw [JetSec.IsHolonomicAt, S.curry_φ] at hS ⊢
   rw [show (S.curry (t, s)).f = fun x ↦ (S.curry (t, s)).f x from rfl, funext (S.curry_f _)]
-  dsimp only
   refine (fderiv.comp x ((S t).f_diff.contDiffAt.differentiableAt le_top)
     ((differentiableAt_const _).prod differentiableAt_id)).trans ?_
   rw [_root_.id, hS]

diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean
@@ -79,7 +79,6 @@ theorem exists_contMDiff_of_convex {P : M → F → Prop} (hP : ∀ x, Convex
   have hPP : ∀ x : M, ReallyConvex (smoothGerm I x) {φ | PP ⟨x, φ⟩} := fun x ↦ by
     apply ReallyConvex.inter
     apply reallyConvex_contMDiffAt
-    dsimp only
     let v : Germ (𝓝 x) F →ₛₗ[smoothGerm.valueRingHom I x] F := Filter.Germ.valueₛₗ I x
     change ReallyConvex (smoothGerm I x) (v ⁻¹' {y | P x y})
     dsimp only [← smoothGerm.valueOrderRingHom_toRingHom] at v
@@ -147,7 +146,6 @@ theorem exists_contMDiff_of_convex₂ {P : M₁ → (M₂ → F) → Prop} [Sigm
   have hPP : ∀ x : M₁, ReallyConvex (smoothGerm I₁ x) {φ | PP ⟨x, φ⟩} := fun x ↦ by
     apply ReallyConvex.inter
     apply reallyConvex_contMDiffAtProd
-    dsimp only
     let v : Germ (𝓝 x) (M₂ → F) →ₛₗ[smoothGerm.valueRingHom I₁ x] M₂ → F := Filter.Germ.valueₛₗ I₁ x
     change ReallyConvex (smoothGerm I₁ x) (v ⁻¹' {y | P x y})
     dsimp only [← smoothGerm.valueOrderRingHom_toRingHom] at v