From 7092ea368025a7c28cd9201bf4b4b76435c3bd69 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 20 Nov 2024 19:57:00 +0100 Subject: [PATCH] chore: fix or silence all multi-goal warnings; small in-passing golfs --- SphereEversion/Global/Immersion.lean | 4 +- SphereEversion/Global/Localisation.lean | 20 +++++----- SphereEversion/Global/OneJetBundle.lean | 5 ++- SphereEversion/Global/OneJetSec.lean | 10 ++--- SphereEversion/Global/Relation.lean | 18 ++++----- SphereEversion/Global/SmoothEmbedding.lean | 2 +- SphereEversion/InductiveConstructions.lean | 19 +++++---- SphereEversion/Local/AmpleRelation.lean | 2 +- SphereEversion/Local/Corrugation.lean | 7 ++-- SphereEversion/Local/SphereEversion.lean | 2 +- SphereEversion/Loops/DeltaMollifier.lean | 10 ++--- SphereEversion/Loops/Exists.lean | 6 +-- SphereEversion/Loops/Reparametrization.lean | 4 +- .../ToMathlib/Algebra/Periodic.lean | 2 +- .../InnerProductSpace/Projection.lean | 39 +++++++++---------- .../Analysis/InnerProductSpace/Rotation.lean | 1 + .../NormedSpace/OperatorNorm/Prod.lean | 5 +-- SphereEversion/ToMathlib/Equivariant.lean | 1 + SphereEversion/ToMathlib/Topology/Misc.lean | 8 ++-- 19 files changed, 81 insertions(+), 84 deletions(-) diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index e1e232e8..42869c9e 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -46,7 +46,7 @@ theorem mem_immersionRel_iff' {σ σ' : OneJetBundle I M I' M'} (hσ' : σ' ∈ σ' ∈ immersionRel I M I' M' ↔ Injective (ψJ σ σ').2 := by simp_rw [mem_immersionRel_iff] rw [oneJetBundle_chartAt_apply, inCoordinates_eq] - simp_rw [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, EquivLike.comp_injective, + · simp_rw [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, EquivLike.comp_injective, EquivLike.injective_comp] exacts [hσ'.1.1, hσ'.1.2] @@ -224,7 +224,7 @@ theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) : ext v erw [mfderiv_neg, ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.neg_apply, smoothStep.of_gt ht] - rw [ω.rot_one]; rfl + rw [ω.rot_one]; · rfl rw [← range_mfderiv_coe_sphere (n := 2) x] exact LinearMap.mem_range_self _ _ diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean index f1cd1dbc..8afe50ea 100644 --- a/SphereEversion/Global/Localisation.lean +++ b/SphereEversion/Global/Localisation.lean @@ -149,22 +149,22 @@ omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in theorem RelLoc.HtpyFormalSol.unloc_congr {𝓕 𝓕' : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {t t' x} (h : 𝓕 t x = 𝓕' t' x) : 𝓕.unloc p t x = 𝓕'.unloc p t' x := by ext1 - rfl - change (𝓕 t x).1 = (𝓕' t' x).1 - rw [h] - change (𝓕 t x).2 = (𝓕' t' x).2 - rw [h] + · rfl + · change (𝓕 t x).1 = (𝓕' t' x).1 + rw [h] + · change (𝓕 t x).2 = (𝓕' t' x).2 + rw [h] omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in theorem RelLoc.HtpyFormalSol.unloc_congr_const {𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {𝓕' : (R.localize p.φ p.ψ).relLoc.FormalSol} {t x} (h : 𝓕 t x = 𝓕' x) : 𝓕.unloc p t x = 𝓕'.unloc x := by ext1 - rfl - change (𝓕 t x).1 = (𝓕' x).1 - rw [h] - change (𝓕 t x).2 = (𝓕' x).2 - rw [h] + · rfl + · change (𝓕 t x).1 = (𝓕' x).1 + rw [h] + · change (𝓕 t x).2 = (𝓕' x).2 + rw [h] omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in theorem RelLoc.HtpyFormalSol.unloc_congr' {𝓕 𝓕' : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {t t'} diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 5eaae7a5..30943130 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -405,7 +405,7 @@ theorem ContinuousAt.inTangentCoordinates_comp {f : N → M} {g : N → M'} {h : simp_rw [inTangentCoordinates, inCoordinates, ContinuousLinearMap.comp_apply] rw [Trivialization.symmL_continuousLinearMapAt] - rfl + · rfl exact hx theorem SmoothAt.clm_comp_inTangentCoordinates {f : N → M} {g : N → M'} {h : N → N'} @@ -525,6 +525,7 @@ theorem SmoothAt.oneJetBundle_map {f : M'' → M → N} {g : M'' → M' → N'} def mapLeft (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) : J¹MM' → OneJetBundle J N I' M' := fun p ↦ OneJetBundle.mk (f p.1.1) p.1.2 (p.2 ∘L Dfinv p.1.1) +set_option linter.style.multiGoal false in omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃] [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in @@ -570,7 +571,7 @@ theorem smooth_bundleSnd : (inTangentCoordinates I (J.prod I) _ _ _ x₀) x₀ := ContMDiffAt.mfderiv (fun (x : OneJetBundle (J.prod I) (N × M) I' M') (y : M) ↦ (x.1.1.1, y)) (fun x : OneJetBundle (J.prod I) (N × M) I' M' ↦ x.1.1.2) ?_ ?_ le_top - exact this + · exact this · exact (smooth_oneJetBundle_proj.fst.fst.prod_map smooth_id).smoothAt -- slow · exact smooth_oneJetBundle_proj.fst.snd.smoothAt diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index edf98b18..023803c4 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -55,7 +55,7 @@ instance : FunLike (OneJetSec I M I' M') M (OneJetBundle I M I' M') where intro S T h dsimp at h ext x - simpa using (Bundle.TotalSpace.mk.inj (congrFun h x)).1 + · simpa using (Bundle.TotalSpace.mk.inj (congrFun h x)).1 have := heq_eq_eq _ _ ▸ (Bundle.TotalSpace.mk.inj (congrFun h x)).2 exact congrFun (congrArg DFunLike.coe this) _ @@ -65,7 +65,7 @@ namespace OneJetSec protected def mk' (F : M → OneJetBundle I M I' M') (hF : ∀ m, (F m).1.1 = m) (h2F : Smooth I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) F) : OneJetSec I M I' M' := - ⟨fun x ↦ (F x).1.2, fun x ↦ (F x).2, by convert h2F using 1; ext m; exact (hF m).symm; rfl; rfl⟩ + ⟨fun x ↦ (F x).1.2, fun x ↦ (F x).2, by convert h2F using 1; ext m; exacts [(hF m).symm, rfl, rfl]⟩ theorem coe_apply (F : OneJetSec I M I' M') (x : M) : F x = ⟨(x, F.bs x), F.ϕ x⟩ := rfl @@ -185,8 +185,8 @@ instance : FunLike (FamilyOneJetSec I M I' M' J N) N (OneJetSec I M I' M') where coe_injective' := by intro S T h ext n : 2 - exact (OneJetSec.mk.inj (congrFun h n)).1 - exact (OneJetSec.mk.inj (congrFun h n)).2 + · exact (OneJetSec.mk.inj (congrFun h n)).1 + · exact (OneJetSec.mk.inj (congrFun h n)).2 namespace FamilyOneJetSec @@ -196,7 +196,7 @@ protected def mk' (FF : N → M → OneJetBundle I M I' M') (hF : ∀ n m, (FF n (h2F : Smooth (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) (uncurry FF)) : FamilyOneJetSec I M I' M' J N := ⟨fun s x ↦ (FF s x).1.2, fun s x ↦ (FF s x).2, - by convert h2F using 1; ext ⟨s, m⟩; exact (hF s m).symm; rfl; rfl⟩ + by convert h2F using 1; ext ⟨s, m⟩; exacts [(hF s m).symm, rfl, rfl]⟩ theorem coe_mk' (FF : N → M → OneJetBundle I M I' M') (hF : ∀ n m, (FF n m).1.1 = m) (h2F : Smooth (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) (uncurry FF)) (x : N) : diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index 644af0a4..79604e3d 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -85,12 +85,12 @@ def mkFormalSol (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x) smooth' := by convert hsmooth ext - rw [hsec] + on_goal 1 => rw [hsec] all_goals rfl is_sol' m := by convert hsol m ext - rw [hsec] + on_goal 1 => rw [hsec] all_goals rfl @[simp] @@ -116,7 +116,7 @@ theorem coe_mk {S : OneJetSec I M I' M'} {h : ∀ x, S x ∈ R} {x : M} : Formal theorem coe_inj_iff {S T : FormalSol R} : S = T ↔ ∀ x, S x = T x := by constructor · rintro rfl x; rfl - · intro h; ext x v : 3; show (S x).1.2 = (T x).1.2; rw [h] + · intro h; ext x v : 3; · show (S x).1.2 = (T x).1.2; rw [h] show (S x).2 v = (T x).2 v; rw [h] theorem coe_inj {S T : FormalSol R} (h : ∀ x, S x = T x) : S = T := @@ -230,8 +230,7 @@ instance : FunLike (FamilyFormalSol J N R) N (FormalSol R) where exact congrArg FormalSol.toOneJetSec (congrFun h n) congr! 1 ext n : 2 - exact (OneJetSec.mk.inj <| fact n).1 - exact (OneJetSec.mk.inj <| fact n).2 + exacts [(OneJetSec.mk.inj <| fact n).1, (OneJetSec.mk.inj <| fact n).2] namespace FamilyFormalSol @@ -280,12 +279,12 @@ def mkHtpyFormalSol (F : ℝ → M → OneJetBundle I M I' M') (hsec : ∀ t x, smooth' := by convert hsmooth using 1 ext ⟨t, x⟩ - exact (hsec t x).symm + · exact (hsec t x).symm all_goals rfl is_sol' t m := by convert hsol t m ext - rw [hsec] + on_goal 1 => rw [hsec] all_goals rfl @[simp] @@ -683,7 +682,7 @@ def Jupdate (F : OneJetSec IM M IN N) (G : HtpyOneJetSec IX X IY Y) (hK : IsComp theorem Jupdate_apply {F : OneJetSec IM M IN N} {G : HtpyOneJetSec IX X IY Y} (hK : IsCompact K) (hFG : ∀ t, ∀ x ∉ K, F (φ x) = (OneJetBundle.embedding φ ψ) (G t x)) (t : ℝ) (m : M) : φ.Jupdate ψ F G hK hFG t m = JΘ F (G t) m := by - ext; exact (φ.Jupdate_aux ψ F (G t) m).symm; rfl; rfl + ext; exacts [(φ.Jupdate_aux ψ F (G t) m).symm, rfl, rfl] theorem Jupdate_bs (F : OneJetSec IM M IN N) (G : HtpyOneJetSec IX X IY Y) (t : ℝ) (hK : IsCompact K) @@ -750,8 +749,7 @@ theorem updateFormalSol_bs {F : FormalSol R} {G : HtpyFormalSol (R.localize φ · simp only [hx, update_of_mem_range, OneJetBundle.embedding_toFun, transfer_proj_snd] rfl · rw [update_of_nmem_range, update_of_nmem_range] - rfl - exacts [hx, hx] + exacts [rfl, hx, hx] @[simp] theorem updateFormalSol_apply_of_mem {F : FormalSol R} {G : HtpyFormalSol (R.localize φ ψ)} diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index a2f5f287..c2ecd3c9 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -261,7 +261,7 @@ def openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : PartialHomeomorph F F} ( IsOpenMap.isOpen_range fun u hu ↦ by have aux : IsOpen (f '' u) := f.isOpen_image_of_subset_source hu (hf₁.symm ▸ subset_univ u) convert isOpen_extChartAt_preimage' x aux - rw [image_comp] + on_goal 1 => rw [image_comp] refine (extChartAt IF x).symm_image_eq_source_inter_preimage ((image_subset_range f u).trans ?_) rw [extChartAt, PartialHomeomorph.extend_target'] diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index 0aad4514..729d2041 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -172,14 +172,13 @@ theorem set_juggling {X : Type*} [TopologicalSpace X] [NormalSpace X] [T2Space X obtain ⟨U', U'_op, hKU', hU'U⟩ : ∃ U' : Set X, IsOpen U' ∧ K ⊆ U' ∧ closure U' ⊆ U := normal_exists_closure_subset hK U_op hKU refine ⟨K₁ ∪ closure (K₂ ∩ U'), K₂ \ U', U₁ ∪ U, U₂ \ K, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ - · exact IsOpen.union U₁_op U_op - · exact IsOpen.sdiff U₂_op hK - · refine IsCompact.union K₁_cpct ?_ + · exact U₁_op.union U_op + · exact U₂_op.sdiff hK + · refine K₁_cpct.union ?_ exact K₂_cpct.closure_of_subset inter_subset_left - · exact IsCompact.diff K₂_cpct U'_op + · exact K₂_cpct.diff U'_op · exact subset_union_left - · apply union_subset_union - exact hK₁U₁ + · apply union_subset_union hK₁U₁ apply subset_trans _ hU'U gcongr exact inter_subset_right @@ -470,8 +469,8 @@ theorem inductive_htpy_construction' {X Y : Type*} ((finite_lt_nat i).isClosed_biUnion fun j _ ↦ (K_cpct j).isClosed) hf₀ hf₁ with ⟨F, hF₀, hF₁, hF₂, hFK₁, ht⟩ refine ⟨F, hF₀, ?_, hF₂, ?_, ht⟩ - apply hF₁.filter_mono - gcongr - rw [bUnion_le] - exact fun t x hx ↦ hFK₁ t x (not_mem_subset K₁W hx) + · apply hF₁.filter_mono + gcongr + rw [bUnion_le] + · exact fun t x hx ↦ hFK₁ t x (not_mem_subset K₁W hx) end Htpy diff --git a/SphereEversion/Local/AmpleRelation.lean b/SphereEversion/Local/AmpleRelation.lean index 065fd8bf..914d62f1 100644 --- a/SphereEversion/Local/AmpleRelation.lean +++ b/SphereEversion/Local/AmpleRelation.lean @@ -57,7 +57,7 @@ def IsAmple (R : RelLoc E F) : Prop := theorem IsAmple.mem_hull (h : IsAmple R) {θ : E × F × (E →L[ℝ] F)} (hθ : θ ∈ R) (v : F) (p) : v ∈ hull (connectedComponentIn (R.slice p θ) (θ.2.2 p.v)) := by rw [h p θ (θ.2.2 p.v)] - exact mem_univ _ + · exact mem_univ _ rw [mem_slice, p.update_self] exact hθ diff --git a/SphereEversion/Local/Corrugation.lean b/SphereEversion/Local/Corrugation.lean index fef8c102..6cac1c77 100644 --- a/SphereEversion/Local/Corrugation.lean +++ b/SphereEversion/Local/Corrugation.lean @@ -197,11 +197,12 @@ theorem Remainder.smooth {γ : G → E → Loop F} (hγ_diff : 𝒞 ∞ ↿γ) { refine (ContDiff.contDiff_top_partial_fst ?_).comp₂ hx.fst' (contDiff_fst.prod contDiff_snd) dsimp [Loop.normalize] apply ContDiff.sub - apply hγ_diff.comp₃ hg.fst'.snd' contDiff_fst contDiff_snd.snd - apply contDiff_average - exact hγ_diff.comp₃ hg.fst'.snd'.fst' contDiff_fst.fst' contDiff_snd + · apply hγ_diff.comp₃ hg.fst'.snd' contDiff_fst contDiff_snd.snd + · apply contDiff_average + exact hγ_diff.comp₃ hg.fst'.snd'.fst' contDiff_fst.fst' contDiff_snd · exact contDiff_const.mul (π.contDiff.comp hx) +set_option linter.style.multiGoal false in theorem remainder_c0_small_on {K : Set E} (hK : IsCompact K) (hγ_diff : 𝒞 1 ↿γ) {ε : ℝ} (ε_pos : 0 < ε) : ∀ᶠ N in atTop, ∀ x ∈ K, ‖R N γ x‖ < ε := by simp_rw [fun N ↦ remainder_eq π N hγ_diff] diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index a367b2be..4d7f0483 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -246,7 +246,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank erw [← this, map_comp] rfl rw [eq, p''.injective_update_iff, mem_compl_iff, eq'] - exact Iff.rfl + · exact Iff.rfl rw [← show ((ℝ ∙ x)ᗮ : Set E).restrict φ = φ.comp j by ext; rfl] exact hφ.injective diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean index 76463711..d1d5b977 100644 --- a/SphereEversion/Loops/DeltaMollifier.lean +++ b/SphereEversion/Loops/DeltaMollifier.lean @@ -51,8 +51,8 @@ def bump (n : ℕ) : ContDiffBump (0 : ℝ) where rIn_pos := by positivity rIn_lt_rOut := by apply one_div_lt_one_div_of_lt - exact_mod_cast Nat.succ_pos _ - exact_mod_cast lt_add_one (n + 2) + · exact_mod_cast Nat.succ_pos _ + · exact_mod_cast lt_add_one (n + 2) theorem support_bump (n : ℕ) : support (bump n) = Ioo (-((1 : ℝ) / (n + 2))) (1 / (n + 2)) := by rw [(bump n).support_eq, Real.ball_eq_Ioo, zero_sub, zero_add, bump] @@ -280,9 +280,9 @@ theorem Loop.mollify_eq_convolution (γ : Loop F) (hγ : Continuous γ) (t : ℝ ((1 : ℝ) / (n + 1)) • ∫ t in (0)..1, γ t := by simp_rw [Loop.mollify, deltaMollifier, add_smul, mul_smul] rw [integral_add] - simp_rw [integral_smul, approxDirac, ← periodize_comp_sub] - rw [intervalIntegral_periodize_smul _ γ _ _ (support_shifted_normed_bump_subset n t)] - simp_rw [MeasureTheory.convolution_eq_swap, ← neg_sub t, (bump n).normed_neg, lsmul_apply] + on_goal 1 => simp_rw [integral_smul, approxDirac, ← periodize_comp_sub] + on_goal 1 => rw [intervalIntegral_periodize_smul _ γ _ _ (support_shifted_normed_bump_subset n t)] + on_goal 1 => simp_rw [MeasureTheory.convolution_eq_swap, ← neg_sub t, (bump n).normed_neg, lsmul_apply] · linarith · rw [zero_add] · exact (continuous_const.smul (((approxDirac_smooth n).continuous.comp diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index 9ea3b40b..de8ce64a 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -202,11 +202,11 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : ((EventuallyEq.rfl.prod_mk <| EventuallyEq.rfl.prod_mk <| (fract_eventuallyEq hs).comp_tendsto continuousAt_id.snd'.snd').fun_comp ↿γ₅) refine ⟨γ, ⟨⟨?_, ?_, ?_, ?_, hγ.continuous⟩, ?_⟩, hγ, ?_⟩ - · intro x t; simp_rw [fract_zero]; rw [hγ₅C]; exact hγ₃.base x _ + · intro x t; simp_rw [fract_zero]; rw [hγ₅C]; · exact hγ₃.base x _ exact Or.inr (by rw [mem_preimage, fract_zero]; exact h0C₁) · intro x s; simp_rw [smoothTransition.zero_of_nonpos le_rfl]; rw [hγ₅C] - exact hγ₃.t₀ x (fract s) - exact Or.inl (show (0 : ℝ) ≤ 5⁻¹ by norm_num) + · exact hγ₃.t₀ x (fract s) + · exact Or.inl (show (0 : ℝ) ≤ 5⁻¹ by norm_num) · intro x t s; simp_rw [smoothTransition_projI] · rintro x -; apply hγε₁; intro s simp_rw [← (γ₃ x 1).fract_eq s, smoothTransition.one_of_one_le le_rfl] diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index e77a95b9..67b14e7c 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -76,9 +76,9 @@ theorem Loop.tendsto_mollify_apply (γ : E → Loop F) (h : Continuous ↿γ) (x · have := h.tendsto (x, t) rw [nhds_prod_eq] at this exact this.comp ((tendsto_fst.comp tendsto_fst).prod_mk tendsto_snd) - · rw [← zero_smul ℝ (_ : F)] - have : Continuous fun z ↦ intervalIntegral (γ z) 0 1 volume := + · have : Continuous fun z ↦ intervalIntegral (γ z) 0 1 volume := intervalIntegral.continuous_parametric_intervalIntegral_of_continuous (by apply h) continuous_const + rw [← zero_smul ℝ (_ : F)] exact (tendsto_one_div_add_atTop_nhds_zero_nat.comp tendsto_snd).smul ((this.tendsto x).comp tendsto_fst) diff --git a/SphereEversion/ToMathlib/Algebra/Periodic.lean b/SphereEversion/ToMathlib/Algebra/Periodic.lean index c1eaf90a..3538fc1d 100644 --- a/SphereEversion/ToMathlib/Algebra/Periodic.lean +++ b/SphereEversion/ToMathlib/Algebra/Periodic.lean @@ -55,7 +55,7 @@ def 𝕊₁ := Quotient transOne deriving TopologicalSpace, Inhabited -theorem transOne_rel_iff {a b : ℝ} : transOne.Rel a b ↔ ∃ k : ℤ, b = a + k := by +theorem transOne_rel_iff {a b : ℝ} : transOne.r a b ↔ ∃ k : ℤ, b = a + k := by refine QuotientAddGroup.leftRel_apply.trans ?_ refine exists_congr fun k ↦ ?_ rw [coe_castAddHom, eq_neg_add_iff_add_eq, eq_comm] diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean index 18507241..924bf794 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean @@ -151,17 +151,16 @@ theorem foo {x₀ x : E} (h : ⟪x₀, x⟫ ≠ 0) (y : E) (hy : y ∈ {.x₀} dsimp only rwa [add_mul, MulZeroClass.zero_mul, div_mul_cancel₀ _ h] +attribute [fun_prop] Continuous.inner + /-- Given two non-orthogonal vectors in an inner product space, `orthogonal_projection_orthogonal_line_iso` is the continuous linear equivalence between their orthogonal complements obtained from orthogonal projection. -/ def orthogonalProjectionOrthogonalLineIso {x₀ x : E} (h : ⟪x₀, x⟫ ≠ 0) : {.x₀}ᗮ ≃L[ℝ] {.x}ᗮ := { - pr[x]ᗮ.comp - (subtypeL - {.x₀}ᗮ) with + pr[x]ᗮ.comp (subtypeL {.x₀}ᗮ) with invFun := fun y ↦ - ⟨y - (⟪x₀, y⟫ / ⟪x₀, x⟫) • x, - by + ⟨y - (⟪x₀, y⟫ / ⟪x₀, x⟫) • x, by rw [mem_orthogonal_span_singleton_iff, inner_sub_right, inner_smul_right] field_simp [h]⟩ left_inv := by @@ -260,24 +259,22 @@ theorem continuousAt_orthogonalProjection_orthogonal {x₀ : E} (hx₀ : x₀ simp only [key] simp_rw [Metric.tendsto_nhds_nhds, Real.dist_0_eq_abs, dist_eq_norm] at lim rcases lim (ε / 2) (half_pos ε_pos) with ⟨η, η_pos, hη⟩ - refine ⟨min (ε / 2 / ‖N x₀‖) (η / 2), ?_, ?_⟩ - · apply lt_min; positivity; exact half_pos η_pos - · intro y hy x - have hy₁ := hy.trans (min_le_left _ _); have hy₂ := hy.trans (min_le_right _ _); clear hy - specialize hη (by linarith : ‖y - x₀‖ < η) - rw [abs_of_nonneg] at hη - calc + refine ⟨min (ε / 2 / ‖N x₀‖) (η / 2), by positivity, ?_⟩ + intro y hy x + have hy₁ := hy.trans (min_le_left _ _); have hy₂ := hy.trans (min_le_right _ _); clear hy + specialize hη (by linarith : ‖y - x₀‖ < η) + rw [abs_of_nonneg (by positivity)] at hη + calc ‖⟪N x₀, x⟫ • (x₀ - y) + ⟪N x₀ - N y, x⟫ • y‖ ≤ ‖⟪N x₀, x⟫ • (x₀ - y)‖ + ‖⟪N x₀ - N y, x⟫ • y‖ := norm_add_le _ _ _ ≤ ‖N x₀‖ * ‖x‖ * ‖x₀ - y‖ + ‖N x₀ - N y‖ * ‖x‖ * ‖y‖ := (add_le_add ?_ ?_) _ ≤ ε / 2 * ‖x‖ + ε / 2 * ‖x‖ := (add_le_add ?_ ?_) _ = ε * ‖x‖ := by linarith - · rw [norm_smul] - exact mul_le_mul_of_nonneg_right (norm_inner_le_norm _ _) (norm_nonneg _) - · rw [norm_smul] - exact mul_le_mul_of_nonneg_right (norm_inner_le_norm _ _) (norm_nonneg _) - · rw [mul_comm, ← mul_assoc, norm_sub_rev] - exact mul_le_mul_of_nonneg_right ((le_div_iff₀ hNx₀).mp hy₁) (norm_nonneg x) - · rw [mul_comm, ← mul_assoc, mul_comm ‖y‖] - exact mul_le_mul_of_nonneg_right hη.le (norm_nonneg x) - · positivity + · rw [norm_smul] + exact mul_le_mul_of_nonneg_right (norm_inner_le_norm _ _) (norm_nonneg _) + · rw [norm_smul] + exact mul_le_mul_of_nonneg_right (norm_inner_le_norm _ _) (norm_nonneg _) + · rw [mul_comm, ← mul_assoc, norm_sub_rev] + exact mul_le_mul_of_nonneg_right ((le_div_iff₀ hNx₀).mp hy₁) (norm_nonneg x) + · rw [mul_comm, ← mul_assoc, mul_comm ‖y‖] + exact mul_le_mul_of_nonneg_right hη.le (norm_nonneg x) diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean index 6ba35ab3..57beac25 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean @@ -130,6 +130,7 @@ open Real Submodule open scoped Real +set_option linter.style.multiGoal false in theorem injOn_rot_of_ne (t : ℝ) {x : E} (hx : x ≠ 0) : Set.InjOn (ω.rot (t, x)) (ℝ ∙ x)ᗮ := by change Set.InjOn (ω.rot (t, x)).toLinearMap (ℝ ∙ x)ᗮ simp_rw [← LinearMap.ker_inf_eq_bot, Submodule.eq_bot_iff, Submodule.mem_inf] diff --git a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean index ddac8c2d..b6b624a8 100644 --- a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean +++ b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean @@ -72,9 +72,8 @@ theorem isBoundedLinearMap_coprod (𝕜 : Type*) [NontriviallyNormedField 𝕜] simp only [Prod.smul_fst, Prod.smul_snd, ContinuousLinearMap.coprod_apply, ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_add] bound := by - refine ⟨2, zero_lt_two, ?_⟩ - rintro ⟨φ, ψ⟩ - apply ContinuousLinearMap.opNorm_le_bound; positivity + refine ⟨2, zero_lt_two, fun ⟨φ, ψ⟩ ↦ ?_⟩ + apply ContinuousLinearMap.opNorm_le_bound _ (by positivity) rintro ⟨e, f⟩ calc ‖φ e + ψ f‖ ≤ ‖φ e‖ + ‖ψ f‖ := norm_add_le _ _ diff --git a/SphereEversion/ToMathlib/Equivariant.lean b/SphereEversion/ToMathlib/Equivariant.lean index 49d82fcf..525f915a 100644 --- a/SphereEversion/ToMathlib/Equivariant.lean +++ b/SphereEversion/ToMathlib/Equivariant.lean @@ -153,6 +153,7 @@ theorem linearReparam_le_one {t : ℝ} (ht : t ≤ 5 / 4) : linearReparam t ≤ theorem one_le_linearReparam {t : ℝ} (ht : 3 / 4 ≤ t) : 1 ≤ linearReparam t := (linearReparam_eq_one le_rfl (by norm_num1)).symm.trans_le (linearReparam_monotone ht) +set_option linter.style.multiGoal false in @[simp] theorem linearReparam_projI {t : ℝ} : linearReparam (projI t) = projI (linearReparam t) := by rw [eq_comm] diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index 16c99b6e..884df87a 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -129,8 +129,8 @@ theorem Ioo_inter_Iio {α : Type*} [LinearOrder α] {a b c : α} : theorem fract_lt {x y : ℝ} {n : ℤ} (h1 : (n : ℝ) ≤ x) (h2 : x < n + y) : fract x < y := by cases' le_total y 1 with hy hy · rw [← fract_sub_int x n, fract_eq_self.mpr] - linarith - constructor <;> linarith + · linarith + · constructor <;> linarith · exact (fract_lt_one x).trans_le hy theorem one_sub_lt_fract {x y : ℝ} {n : ℤ} (hy : y ≤ 1) (h1 : (n : ℝ) - y < x) (h2 : x < n) : @@ -139,8 +139,8 @@ theorem one_sub_lt_fract {x y : ℝ} {n : ℤ} (hy : y ≤ 1) (h1 : (n : ℝ) - have I₂ : x - (n - 1) < 1 := by linarith norm_cast at I₁ I₂ rw [← fract_sub_int x (n - 1), fract_eq_self.mpr] - exact I₁ - constructor <;> linarith + · exact I₁ + · constructor <;> linarith theorem IsOpen.preimage_fract' {s : Set ℝ} (hs : IsOpen s) (h2s : 0 ∈ s → s ∈ 𝓝[<] (1 : ℝ)) : IsOpen (fract ⁻¹' s) := by