diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index af4fc2a2..c4b71d71 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -50,7 +50,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] @@ -62,7 +62,7 @@ set_option backward.isDefEq.respectTransparency false in theorem immersionRel_open [FiniteDimensional ℝ E] : IsOpen (immersionRel I M I' M') := by simp_rw [ChartedSpace.isOpen_iff HJ (immersionRel I M I' M'), chartAt_image_immersionRel_eq] refine fun σ ↦ (ψJ σ).open_target.inter ?_ - convert isOpen_univ.prod ContinuousLinearMap.isOpen_injective + convert! isOpen_univ.prod ContinuousLinearMap.isOpen_injective · ext x -- Porting note: `mem_prod` is a simp lemma, but the next line is still needed. rw [mem_prod] @@ -228,8 +228,8 @@ theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) : · congr 2 with y simp [smoothStep.of_gt ht] ext v - erw [mfderiv_neg, ContinuousLinearMap.coe_comp', Function.comp_apply, - ContinuousLinearMap.neg_apply, smoothStep.of_gt ht] + erw [mfderiv_neg, ContinuousLinearMap.coe_comp, Function.comp_apply, _root_.neg_apply, + smoothStep.of_gt ht] rw [ω.rot_one]; · rfl rw [← range_mfderiv_coe_sphere (n := 2) x] exact LinearMap.mem_range_self .. @@ -325,12 +325,12 @@ theorem sphere_eversion : refine ⟨f, h₁, ?_, ?_, ?_/-h₅-/⟩ · ext x rw [this (0, x) (by simp)] - convert formalEversion_zero E ω x + convert! formalEversion_zero E ω x · ext x rw [this (1, x) (by simp)] - convert formalEversion_one E ω x + convert! formalEversion_one E ω x · exact fun t ↦ { - contMDiff := ContMDiff.uncurry_left 𝓘(ℝ, ℝ) (𝓡 2) 𝓘(ℝ, E) h₁ t + contMDiff := h₁.uncurry_left 𝓘(ℝ, ℝ) (𝓡 2) 𝓘(ℝ, E) t diff_injective := h₅ t } diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index e1d946fc..361db366 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -112,7 +112,7 @@ variable (I I') instance (p : M × M') : FunLike (OneJetSpace I I' p) (TangentSpace I p.1) (TangentSpace I' p.2) where coe := fun φ ↦ φ.toFun - coe_injective' := fun _ _ h ↦ ContinuousLinearMap.ext (congrFun h) + coe_injective := fun _ _ h ↦ ContinuousLinearMap.ext (congrFun h) variable (M M') @@ -243,7 +243,7 @@ theorem oneJetBundle_chart_source (x₀ : J¹MM') : PartialEquiv.trans_source, OpenPartialHomeomorph.prod_toPartialEquiv, PartialEquiv.prod_source, - OpenPartialHomeomorph.coe_coe, + OpenPartialHomeomorph.coe_toPartialEquiv, Trivialization.coe_coe, OpenPartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_source, @@ -278,10 +278,10 @@ end section variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} -[NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] -{H : Type*} [TopologicalSpace H] {H' : Type*} [TopologicalSpace H'] -{I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type*} [TopologicalSpace M] -[ChartedSpace H M] {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} + [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] + {H : Type*} [TopologicalSpace H] {H' : Type*} [TopologicalSpace H'] + {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {M : Type*} [TopologicalSpace M] + [ChartedSpace H M] {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] {n : ℕ∞} @[simp] lemma ContMDiffMap.coe_fst : @@ -615,7 +615,7 @@ theorem oneJetBundle_model_space_chartAt (p : OneJetBundle I H I' H') : (Bundle.TotalSpace.toProd (H × H') (E →L[𝕜] E')).toPartialEquiv := by apply partialEquiv_eq_equiv · intro x - rw [OpenPartialHomeomorph.coe_coe, oneJetBundle_chartAt_apply p x, + rw [OpenPartialHomeomorph.coe_toPartialEquiv, oneJetBundle_chartAt_apply p x, inCoordinates_tangent_bundle_core_model_space] ext <;> rfl · simp_rw [oneJetBundle_chart_source, prodChartedSpace_chartAt, chartAt_self_eq, @@ -641,7 +641,7 @@ theorem oneJetBundle_model_space_coe_chartAt_symm (p : OneJetBundle I H I' H') : ext x · rfl · rfl - · rw [← OpenPartialHomeomorph.coe_coe_symm, oneJetBundle_model_space_chartAt] + · rw [← OpenPartialHomeomorph.coe_toPartialEquiv_symm, oneJetBundle_model_space_chartAt] rfl variable (I I') diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index 865d2633..6b8fd28b 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -53,7 +53,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] instance : FunLike (OneJetSec I M I' M') M (OneJetBundle I M I' M') where coe := fun S x ↦ OneJetBundle.mk x (S.bs x) (S.ϕ x) - coe_injective' := by + coe_injective := by intro S T h dsimp at h ext x @@ -186,7 +186,7 @@ instance : FunLike (FamilyOneJetSec I M I' M' J N) N (OneJetSec I M I' M') where { bs := S.bs t ϕ := S.ϕ t contMDiff' x := (S.contMDiff' (t, x)).comp x <| contMDiffAt_const.prodMk contMDiffAt_id } - coe_injective' := by + coe_injective := by intro S T h ext n : 2 · exact (OneJetSec.mk.inj (congrFun h n)).1 diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index c821076a..8dcd0291 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -142,11 +142,11 @@ theorem FamilyOneJetSec.uncurry_mem_relativize (S : FamilyOneJetSec I M I' M' IP -- Porting note: we are missing an ext lemma here. apply ContinuousLinearMap.ext_iff.2 (fun v ↦ ?_) change ((S.uncurry.ϕ (s, x)).comp (ContinuousLinearMap.inr ℝ EP E)) v = _ - erw [S.uncurry_ϕ', ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply, + erw [S.uncurry_ϕ', ContinuousLinearMap.comp_apply, add_apply, ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.comp_apply] -- adaptation note: in Lean 4.28, all this proof was just `simp` - simp only [uncurry_bs, bs_eq_coe_bs, add_eq_right] + simp only [bs_eq_coe_bs, add_eq_right] exact ContinuousLinearMap.map_zero _ def FamilyFormalSol.uncurry (S : FamilyFormalSol IP P R) : FormalSol (R.relativize IP P) := by @@ -223,7 +223,7 @@ set_option backward.isDefEq.respectTransparency false in theorem FamilyOneJetSec.curry_mem (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) {p : N × P} {x : M} (hR : S p.1 (p.2, x) ∈ R.relativize IP P) : S.curry p x ∈ R := by simp_rw [RelMfld.relativize, mem_preimage, bundleSnd_eq, OneJetSec.coe_apply, mapLeft] at hR ⊢ - convert hR + convert! hR -- Porting note: we are missing an ext lemma here. apply ContinuousLinearMap.ext_iff.2 (fun v ↦ ?_) rw [S.curry_ϕ'] @@ -244,7 +244,7 @@ theorem curry_eq_iff_eq_uncurry {𝓕 : FamilyFormalSol J N (R.relativize IP P)} refine ⟨h.1, ?_⟩ rw [𝓕.curry_ϕ', h.2, 𝓕₀.uncurry_ϕ'] ext v - erw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply, + erw [ContinuousLinearMap.comp_apply, add_apply, ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.comp_apply, ContinuousLinearMap.coe_snd', ContinuousLinearMap.map_zero, zero_add] diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index a5eb42c9..5c97d5e3 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -71,11 +71,11 @@ structure FormalSol (R : RelMfld I M I' M') extends OneJetSec I M I' M' where set_option backward.isDefEq.respectTransparency false in instance (R : RelMfld I M I' M') : FunLike (FormalSol R) M (OneJetBundle I M I' M') where coe := fun F ↦ F.toOneJetSec - coe_injective' := by + coe_injective := by intro F G h ext x : 2 · exact congrArg Prod.snd (congrArg Bundle.TotalSpace.proj (congrFun h x)) - · simpa using (Bundle.TotalSpace.ext_iff.mp (congrFun h x)).2 + · simpa using! (Bundle.TotalSpace.ext_iff.mp (congrFun h x)).2 def mkFormalSol (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x) (hsol : ∀ x, F x ∈ R) (hsmooth : ContMDiff I ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ F) : FormalSol R @@ -191,7 +191,7 @@ theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} ext1 w rw [mem_slice] change _ ↔ OneJetBundle.mk σ.proj.1 σ.proj.2 (DualPair.update p σ.snd w) ∈ R - convert Iff.rfl using 3 + convert! Iff.rfl using 3 rw [oneJetBundle_mk_snd, p.update_update] /-- A differential relation is ample if all its slices are ample sets. -/ @@ -219,7 +219,7 @@ structure FamilyFormalSol (R : RelMfld I M I' M') extends FamilyOneJetSec I M I' instance : FunLike (FamilyFormalSol J N R) N (FormalSol R) where coe := fun S n ↦ ⟨S.toFamilyOneJetSec n, S.is_sol' n⟩ - coe_injective' := by + coe_injective := by intro S T rcases S with ⟨S, -⟩ rcases T with ⟨T, -⟩ @@ -634,7 +634,7 @@ def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where · rw [OpenSmoothEmbedding.invFun_comp_coe] · rw [OpenSmoothEmbedding.invFun_comp_coe] · ext x v; simp_rw [ContinuousLinearMap.comp_apply] - convert (φ.fderiv x).symm_apply_apply v + convert! (φ.fderiv x).symm_apply_apply v erw [φ.left_inv]; rfl isOpen_range := φ.isOpen_range_transfer ψ contMDiff_to := φ.smooth_transfer ψ diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index 2608dbe8..ba2618c0 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -253,11 +253,7 @@ def openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : OpenPartialHomeomorph F left_inv' {y} := by obtain ⟨z, hz, hz'⟩ := hf₄ (mem_range_self y) have aux : f.symm (IF z) = y := by rw [hz']; exact f.left_inv (hf₁.symm ▸ mem_univ _) - simp only [← hz', (chartAt H x).right_inv hz, extChartAt, OpenPartialHomeomorph.extend, - PartialEquiv.coe_trans, OpenPartialHomeomorph.invFun_eq_coe, - ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe, - PartialEquiv.coe_trans_symm, OpenPartialHomeomorph.coe_coe_symm, - ModelWithCorners.left_inv, ModelWithCorners.toPartialEquiv_coe_symm, Function.comp_apply, aux] + simp [← hz', (chartAt H x).right_inv hz, aux] isOpen_range := IsOpenMap.isOpen_range fun u hu ↦ by have aux : IsOpen (f '' u) := f.isOpen_image_of_subset_source hu (hf₁.symm ▸ subset_univ u) @@ -347,7 +343,7 @@ theorem nice_atlas' {ι : Type*} {s : ι → Set M} (s_op : ∀ j, IsOpen <| s j rintro ⟨⟨x, r⟩, hxr⟩ obtain ⟨hr : 0 < r, -, -⟩ := ht₂ _ hxr exact monotone_image (range_diffeomorphToNhd_subset_ball _ hr) - · simpa only [iUnion_coe_set] using ht₃ + · simpa only [iUnion_coe_set] using! ht₃ variable [Nonempty M] diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index ee373030..efe62c8b 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -89,7 +89,7 @@ variable {I M V} instance : DFunLike (OneJetEuclSec I M V) M fun _ ↦ J¹[𝕜, E, I, M, V] where coe := OneJetEuclSec.toFun - coe_injective' := by + coe_injective := by intro S T h ext x <;> rw [h] @@ -190,7 +190,7 @@ structure FamilyOneJetEuclSec where instance : FunLike (FamilyOneJetEuclSec I M V J N) (N × M) J¹[ℝ, E, I, M, V] where coe := FamilyOneJetEuclSec.toFun - coe_injective' := by + coe_injective := by intro S T h ext x <;> rw [h] @@ -230,6 +230,6 @@ def familyTwist (s : OneJetEuclSec I M V) (i : N × M → V →L[ℝ] V') have : ContMDiffAt (J.prod I) _ ∞ (fun x : N × M ↦ _) x₀ := s.contMDiff.comp contMDiff_snd x₀ rw [contMDiffAt_one_jet_eucl_bundle'] at this refine (hi x₀).clm_comp ?_ - convert this.2 <;> simp [s.is_sec] + convert! this.2 <;> simp [s.is_sec] end familyTwist diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index f83ce45f..9e40a70b 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -170,7 +170,7 @@ theorem set_juggling {X : Type*} [TopologicalSpace X] [NormalSpace X] [T2Space X normal_exists_closure_subset hK U_op hKU refine ⟨K₁ ∪ closure (K₂ ∩ U'), K₂ \ U', U₁ ∪ U, U₂ \ K, U₁_op.union U_op, U₂_op.sdiff hK, ?_, K₂_cpct.diff U'_op, subset_union_left, - ?_, by gcongr, ?_, by grind, ?_, diff_subset⟩ + ?_, by gcongr, ?_, by grind, ?_, sdiff_subset⟩ · exact K₁_cpct.union (K₂_cpct.closure_of_subset inter_subset_left) · gcongr; grw [← hU'U] gcongr @@ -178,8 +178,8 @@ theorem set_juggling {X : Type*} [TopologicalSpace X] [NormalSpace X] [T2Space X · rw [union_assoc] congr apply subset_antisymm - · exact union_subset (K₂_cpct.isClosed.closure_subset_iff.mpr inter_subset_left) diff_subset - · calc K₂ = K₂ ∩ U' ∪ K₂ \ U' := (inter_union_diff K₂ U').symm + · exact union_subset (K₂_cpct.isClosed.closure_subset_iff.mpr inter_subset_left) sdiff_subset + · calc K₂ = K₂ ∩ U' ∪ K₂ \ U' := (inter_union_sdiff K₂ U').symm _ ⊆ closure (K₂ ∩ U') ∪ K₂ \ U' := union_subset_union_left (K₂ \ U') subset_closure · rw [union_comm] @@ -366,7 +366,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ · rintro (rfl : t = 0) exact (lt_irrefl _ ((T_nonneg i.toNat).trans_lt ht)).elim · simpa only [mul_sub, neg_mul] - using hP₂ ((2 : ℝ) ^ (i.toNat + 1)) (-(2 : ℝ) ^ (i.toNat + 1) * T i.toNat) + using! hP₂ ((2 : ℝ) ^ (i.toNat + 1)) (-(2 : ℝ) ^ (i.toNat + 1) * T i.toNat) (t, x) (↿F') (h₂F' _) · intro hi x t ht rw [i.toNat_succ hi] at ht ⊢ diff --git a/SphereEversion/Local/Corrugation.lean b/SphereEversion/Local/Corrugation.lean index 21125488..4a42ec65 100644 --- a/SphereEversion/Local/Corrugation.lean +++ b/SphereEversion/Local/Corrugation.lean @@ -183,8 +183,8 @@ theorem fderiv_corrugated_map (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) {f : E ext v erw [fderiv_add (hf.differentiable (by simp)).differentiableAt ((corrugation.contDiff _ N hγ_diff).differentiable (by simp)).differentiableAt] - simp_rw [ContinuousLinearMap.add_apply, corrugation.fderiv_apply _ N hN hγ_diff, hfγ, - DualPair.update, ContinuousLinearMap.add_apply, p.π.comp_toSpanSingleton_apply, add_assoc] + simp_rw [add_apply, corrugation.fderiv_apply _ N hN hγ_diff, hfγ, + DualPair.update, add_apply, p.π.comp_toSpanSingleton_apply, add_assoc] open scoped ContDiff @@ -195,7 +195,6 @@ theorem Remainder.smooth {γ : G → E → Loop F} (hγ_diff : 𝒞 ∞ ↿γ) { · let ψ : E → H × ℝ → F := fun x q ↦ (γ (g q.1) x).normalize q.2 change 𝒞 ∞ fun q : H × ℝ ↦ ∂₁ ψ (x q.1) (q.1, q.2) refine (ContDiff.contDiff_top_partial_fst ?_).comp₂ hx.fst' (contDiff_fst.prodMk contDiff_snd) - dsimp [Loop.normalize] apply ContDiff.sub · apply hγ_diff.comp₃ hg.fst'.snd' contDiff_fst contDiff_snd.snd · apply contDiff_average diff --git a/SphereEversion/Local/DualPair.lean b/SphereEversion/Local/DualPair.lean index 808e7de9..b8cce50e 100644 --- a/SphereEversion/Local/DualPair.lean +++ b/SphereEversion/Local/DualPair.lean @@ -101,7 +101,7 @@ theorem update_self (p : DualPair E) (φ : E →L[ℝ] F) : p.update φ (φ p.v) @[simp] theorem update_update (p : DualPair E) (φ : E →L[ℝ] F) (w w' : F) : p.update (p.update φ w') w = p.update φ w := by - simp_rw [update, add_apply, coe_comp', (· ∘ ·), toSpanSingleton_apply, p.pairing, one_smul, + simp_rw [update, add_apply, coe_comp, (· ∘ ·), toSpanSingleton_apply, p.pairing, one_smul, add_sub_cancel, add_assoc, ← ContinuousLinearMap.add_comp, ← toSpanSingleton_add, sub_add_eq_add_sub, add_sub_cancel] diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean index 87ce6f5c..8ab338a4 100644 --- a/SphereEversion/Local/HPrinciple.lean +++ b/SphereEversion/Local/HPrinciple.lean @@ -372,13 +372,12 @@ theorem improveStep_part_hol {N : ℝ} (hN : N ≠ 0) : rcases Submodule.mem_span_singleton.mp hu with ⟨l, rfl⟩ rw [(D 𝓕'.f x).map_smul, (𝓕'.φ x).map_smul] apply congr_arg - erw [fderiv_𝓕', ContinuousLinearMap.add_apply, L.p.update_v, ContinuousLinearMap.add_apply, - L.p.update_v] + erw [fderiv_𝓕', add_apply, L.p.update_v, add_apply, L.p.update_v] rfl · intro u hu have hu_ker := L.hEp hu - erw [fderiv_𝓕', ContinuousLinearMap.add_apply, L.p.update_ker_pi _ _ hu_ker, - ContinuousLinearMap.add_apply, L.p.update_ker_pi _ _ hu_ker, hx u hu] + erw [fderiv_𝓕', add_apply, L.p.update_ker_pi _ _ hu_ker, + add_apply, L.p.update_ker_pi _ _ hu_ker, hx u hu] theorem improveStep_formalSol : ∀ᶠ N in atTop, ∀ t, (L.improveStep h N t).IsFormalSol R := by set γ := L.loop h @@ -486,7 +485,7 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C { L with E' := E' k.castSucc p := e.dualPair k - hEp := by simpa only [E', Module.Basis.dualPair] using e.flag_le_ker_dual k } + hEp := by simpa only [E', Module.Basis.dualPair] using! e.flag_le_ker_dual k } set H₁ : FormalSol R := (hH_sol 1).formalSol have h_span : E' k.succ = S.p.spanV ⊔ S.E' := e.flag_succ k have acc : S.Accepts R H₁ := diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean index a4c0edff..7724e567 100644 --- a/SphereEversion/Local/OneJet.lean +++ b/SphereEversion/Local/OneJet.lean @@ -57,7 +57,7 @@ variable {E F} instance : FunLike (JetSec E F) E (F × (E →L[ℝ] F)) where coe 𝓕 := fun x ↦ (𝓕.f x, 𝓕.φ x) - coe_injective' := by + coe_injective := by rintro ⟨⟩ ⟨⟩ h; congr exacts [congr_arg (Prod.fst ∘ ·) h, congr_arg (Prod.snd ∘ ·) h] @@ -149,7 +149,7 @@ instance : FunLike (FamilyJetSec E F P) P (JetSec E F) where f_diff := S.f_diff.comp (contDiff_const.prodMk contDiff_id) φ := S.φ t φ_diff := S.φ_diff.comp (contDiff_const.prodMk contDiff_id) } - coe_injective' := by + coe_injective := by rintro ⟨⟩ ⟨⟩ h simp only [funext_iff, DFunLike.ext_iff, JetSec.mk_apply, Prod.ext_iff] at h congr <;> ext <;> simp [h] diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean index 90a3efe1..04059ca6 100644 --- a/SphereEversion/Local/ParametricHPrinciple.lean +++ b/SphereEversion/Local/ParametricHPrinciple.lean @@ -151,7 +151,7 @@ theorem FamilyJetSec.uncurry_mem_relativize (S : FamilyJetSec E F P) {s : P} {x (ContinuousLinearMap.inr ℝ P E) = JetSec.φ (S s) x by rw [this]; rfl ext v - simp_rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply, + simp_rw [ContinuousLinearMap.comp_apply, add_apply, ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', ContinuousLinearMap.map_zero, zero_add] rfl @@ -248,7 +248,7 @@ theorem curry_eq_iff_eq_uncurry_loc {𝓕 : FamilyFormalSol G (R.relativize P)} change ((D (fun (z : P) ↦ 𝓕₀.toFamilyJetSec.f z x) s).comp (fst ℝ P E) + (𝓕₀.toFamilyJetSec.φ s x).comp (snd ℝ P E)).comp (inr ℝ P E) = ((𝓕₀ s) x).snd ext v - simp_rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply, + simp_rw [ContinuousLinearMap.comp_apply, add_apply, ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', ContinuousLinearMap.map_zero, zero_add] rfl diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index 76d171f3..247dcd86 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -121,7 +121,7 @@ theorem loc_immersion_rel_open_aux {x₀ : E} {y₀ : F} {φ₀ : E →L[ℝ] F} constructor · change ⟪x₀, x₀⟫ ≠ 0 apply inner_self_eq_zero.not.mpr x₀_ne - · change Injective (φ₀ ∘ (Subtype.val : (ℝ ∙ x₀)ᗮ → E) ∘ (orthogonalProjection (ℝ ∙ x₀)ᗮ) ∘ + · change Injective (φ₀ ∘ (Subtype.val : (ℝ ∙ x₀)ᗮ → E) ∘ (orthogonalProjectionOnto (ℝ ∙ x₀)ᗮ) ∘ (Subtype.val : (ℝ ∙ x₀)ᗮ → E)) erw [orthogonalProjection_comp_coe, comp_id] exact injOn_iff_injective.mp H @@ -220,7 +220,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank erw [inf_left_right_swap, inf_comm, ← inf_assoc, p'.inf_eq_bot, bot_inf_eq] have eq₃ : dim (span ℝ {v'}) = 1 := finrank_span_singleton p'.v_ne_zero rw [← hv', eq₁, eq₃, eq₂] at eq - simpa only [finrank_bot] using eq.symm + simpa only [finrank_bot] using! eq.symm have : dim E = n + 1 := Fact.out linarith [finrank_map_le Φ (p.π.ker ⊓ (ℝ ∙ x)ᗮ)] ext w @@ -230,8 +230,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank let p'' : DualPair (ℝ ∙ x)ᗮ := ⟨p.π.comp j, ⟨v', v'_in⟩, hπv'⟩ have eq : ((ℝ ∙ x)ᗮ : Set E).restrict (p'.update φ w) = p''.update (φ.comp j) w := by ext z - simp only [p', j, DualPair.update, restrict_apply, ContinuousLinearMap.add_apply, p'', - ContinuousLinearMap.coe_comp', coe_subtypeL, Submodule.coe_subtype, comp_apply] + simp [p', j, DualPair.update, p''] have eq' : (p''.π.ker).map (φ.comp j : _ →ₛₗ[.id ℝ] F) = (p.π.ker ⊓ (ℝ ∙ x)ᗮ).map (φ : E →ₛₗ[.id ℝ] F) := by have : (p''.π.ker).map (j : _ →ₛₗ[.id ℝ] _) = p.π.ker ⊓ (ℝ ∙ x)ᗮ := by @@ -253,7 +252,7 @@ end AssumeFiniteDimensional /-- The main ingredient of the linear map in the formal eversion of the sphere. -/ def locFormalEversionAuxφ [Fact (dim E = 3)] (ω : Orientation ℝ E (Fin 3)) (t : ℝ) (x : E) : E →L[ℝ] E := - ω.rot (t, x) - (2 * t) • Submodule.subtypeL (ℝ ∙ x) ∘L orthogonalProjection (ℝ ∙ x) + ω.rot (t, x) - (2 * t) • Submodule.subtypeL (ℝ ∙ x) ∘L orthogonalProjectionOnto (ℝ ∙ x) section AssumeFiniteDimensional local notation "∞" => ((⊤ : ℕ∞) : WithTop ℕ∞) @@ -333,10 +332,8 @@ def locFormalEversion : HtpyFormalSol (immersionSphereRel E E) := have h3x : x ≠ 0 := by rintro rfl; apply hx; exact mem_ball_self (by norm_num) refine (EqOn.injOn_iff ?_).mpr (ω.injOn_rot_of_ne (smoothStep t) h3x) intro v hv - simp_rw [locFormalEversionAuxφ, ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply, - ContinuousLinearMap.comp_apply, - orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hv, _root_.map_zero, - smul_zero, sub_zero] } + simp_rw [locFormalEversionAuxφ, sub_apply, smul_apply, ContinuousLinearMap.comp_apply, + orthogonalProjectionOnto_apply_of_mem_orthogonal hv, _root_.map_zero, smul_zero, sub_zero] } @[simp] theorem locFormalEversion_f (t : ℝ) : @@ -346,7 +343,7 @@ theorem locFormalEversion_f (t : ℝ) : theorem locFormalEversion_φ (t : ℝ) (x : E) (v : E) : (locFormalEversion ω t).φ x v = smoothStep (‖x‖ ^ 2) • - (ω.rot (smoothStep t, x) v - (2 * smoothStep t) • orthogonalProjection (ℝ ∙ x) v) := + (ω.rot (smoothStep t, x) v - (2 * smoothStep t) • orthogonalProjectionOnto (ℝ ∙ x) v) := rfl theorem locFormalEversion_zero (x : E) : (locFormalEversion ω 0).f x = x := by @@ -368,11 +365,11 @@ theorem locFormalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) {x : E} (hx : smoot locFormalEversion_φ, smoothStep.of_gt ht, hx] intro v have : (fun x : E ↦ ((1 : ℝ) - 2) • x) = fun x ↦ -x := by ext x; norm_num - simp only [mul_one, this, coe_orthogonalProjection_apply, one_smul] + simp only [mul_one, this, coe_orthogonalProjectionOnto_apply, one_smul] obtain ⟨v', hv', v, hv, rfl⟩ := Submodule.exists_add_mem_mem_orthogonal (K := ℝ ∙ x) v simp_rw [ContinuousLinearMap.map_add, ω.rot_one _ hv, ω.rot_eq_of_mem_span (1, x) hv'] rw [fderiv_fun_neg, fderiv_fun_id] - simp only [ContinuousLinearMap.neg_apply, ContinuousLinearMap.coe_id', id_eq, add_zero, + simp only [neg_apply, ContinuousLinearMap.coe_id', id_eq, add_zero, starProjection_eq_self_iff.mpr hv', two_smul, add_sub_add_left_eq_sub, (Submodule.starProjection_apply_eq_zero_iff _).mpr hv] abel diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean index aaeb7690..79f4fea7 100644 --- a/SphereEversion/Loops/Basic.lean +++ b/SphereEversion/Loops/Basic.lean @@ -106,7 +106,7 @@ theorem range_eq_image (γ : Loop X) : range γ = γ '' I := by /-- Transforming a loop by applying function `f`. -/ @[simps] def transform (γ : Loop X) (f : X → X') : Loop X' := - ⟨fun t ↦ f (γ t), fun t ↦ by dsimp only; rw [γ.per]⟩ + ⟨fun t ↦ f (γ t), fun t ↦ by rw [γ.per]⟩ /-- Adding two loops pointwise. -/ @[simps] diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index 6d9f9fe6..f767284f 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -183,7 +183,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : obtain ⟨γ₅, hγ₅, hγ₅₄, hγ₅C⟩ := exists_smooth_and_eqOn hγ₄ hcε₂.fst' (fun x ↦ hε₂) hC ⟨U, hUC, h3γ₄⟩ let γ : E → ℝ → Loop F := fun x t ↦ - ⟨fun s ↦ γ₅ (x, smoothTransition t, fract s), fun s ↦ by dsimp; rw [fract_add_one s]⟩ + ⟨fun s ↦ γ₅ (x, smoothTransition t, fract s), fun s ↦ by rw [fract_add_one s]⟩ have hγ : 𝒞 ∞ ↿γ := by rw [contDiff_iff_contDiffAt] rintro ⟨x, t, s⟩; by_cases hs : fract s = 0 diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index b7adbedb..1e6639c0 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -248,7 +248,7 @@ theorem localCenteringDensity_pos (hy : y ∈ γ.localCenteringDensityNhd x) (t simp only [γ.localCenteringDensity_spec x, Fintype.sum_apply, Pi.smul_apply, smul_eq_mul] refine Finset.sum_pos (fun i _ ↦ mul_pos ?_ (deltaMollifier_pos _)) Finset.univ_nonempty obtain ⟨w, hw⟩ := γ.approxSurroundingPointsAt_of_localCenteringDensityNhd x y hy - convert hw.w_pos i + convert! hw.w_pos i rw [← hw.coord_eq_w] simp [evalBarycentricCoords, γ.approxSurroundingPointsAt_mem_affineBases x y hy] diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index 391e973f..7dd0d5a1 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -226,7 +226,7 @@ theorem smooth_surrounding [FiniteDimensional ℝ F] {x : F} {p : ι → F} {w : have hyq' : (y, q) ∈ W' ⁻¹' V := inter_subset_right hyq refine ⟨⟨U, mem_nhds_iff.mpr ⟨U, le_refl U, hU₂, hyq⟩, ((smooth_barycentric ι ℝ F hι).mono inter_subset_left).of_le le_top⟩, ?_, ?_, ?_⟩ - · simpa [V] using hyq' + · simpa [V] using! hyq' · simp [hq] · simp only [hq, evalBarycentricCoords_apply_of_mem_bases, AffineBasis.coords_apply] exact AffineBasis.linear_combination_coord_eq_self _ y @@ -255,7 +255,7 @@ theorem surroundingPts_evalBarycentricCoords_iff (q : F) (v : ι → F) refine ⟨hv.1, h, hv', ?_⟩ simp_rw [← Finset.univ.affineCombination_eq_linear_combination v _ hv', evalBarycentricCoords_apply_of_mem_bases ι ℝ F q hv] - convert AffineBasis.affineCombination_coord_eq_self _ q + convert! AffineBasis.affineCombination_coord_eq_self _ q rfl end SurroundingPoints @@ -356,7 +356,7 @@ theorem zero_vadd : (0 : F) +ᵥ γ = γ := by theorem vadd_surrounds : γ.Surrounds x ↔ (y +ᵥ γ).Surrounds (y + x) := by rw [add_comm] - convert affineEquiv_surrounds_iff (AffineEquiv.vaddConst ℝ y) using 2 + convert! affineEquiv_surrounds_iff (AffineEquiv.vaddConst ℝ y) using 2 ext u simp [add_comm y] @@ -383,7 +383,7 @@ theorem Surrounds.mono (h : γ.Surrounds x) (h2 : range γ ⊆ range γ') : γ'. protected theorem Surrounds.reparam (h : γ.Surrounds x) {φ : EquivariantMap} (hφ : Continuous φ) : (γ.reparam φ).Surrounds x := by refine h.mono ?_ - convert subset_of_eq (range_comp γ φ).symm + convert! subset_of_eq (range_comp γ φ).symm rw [(φ.surjective hφ).range_eq, image_univ] /-- This is only a stepping stone potentially useful for `SurroundingFamily.surrounds_of_close`, @@ -878,7 +878,7 @@ theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁ have hV₀L₁ : Disjoint (closure V₀) L₁ := disjoint_sdiff_self_right.mono hVU₀ Subset.rfl obtain ⟨V₂, hV₂, hLV₂, h2V₂⟩ := normal_exists_closure_subset hL₁ (isClosed_closure.isOpen_compl.inter hU₁) - (subset_inter (subset_compl_iff_disjoint_left.mpr hV₀L₁) <| diff_subset.trans hKU₁) + (subset_inter (subset_compl_iff_disjoint_left.mpr hV₀L₁) <| sdiff_subset.trans hKU₁) obtain ⟨V₁, hV₁, hLV₁, hV₁₂⟩ := normal_exists_closure_subset hL₁ hV₂ hLV₂ rw [subset_inter_iff, subset_compl_iff_disjoint_left] at h2V₂ rcases h2V₂ with ⟨hV₀₂, hV₂U₁⟩ @@ -888,7 +888,7 @@ theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁ rw [← subset_compl_iff_disjoint_left, compl_compl]; exact hV₁₂ refine ⟨V₀ ∪ U₁ ∩ U₀ ∪ V₁, ((hV₀.union <| hU₁.inter hU₀).union hV₁).mem_nhdsSet.mpr ?_, ?_⟩ · refine union_subset (hKV₀.trans <| subset_union_left.trans <| subset_union_left) ?_ - rw [← inter_union_diff K₁]; + rw [← inter_union_sdiff K₁]; exact union_subset_union ((inter_subset_inter_left _ hKU₁).trans <| subset_union_right) hLV₁ obtain ⟨ρ, h0ρ, h1ρ, -⟩ := exists_continuous_zero_one_of_isClosed (isClosed_closure.union hV₂.isClosed_compl) diff --git a/SphereEversion/ToMathlib/Analysis/ContDiff.lean b/SphereEversion/ToMathlib/Analysis/ContDiff.lean index 91d1bd43..6da0e5b0 100644 --- a/SphereEversion/ToMathlib/Analysis/ContDiff.lean +++ b/SphereEversion/ToMathlib/Analysis/ContDiff.lean @@ -213,7 +213,7 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Complete -- variant of `Submodule.orthogonalProjection_singleton` theorem Submodule.orthogonalProjection_singleton' {v : E} : - (𝕜 ∙ v).subtypeL.comp (orthogonalProjection (𝕜 ∙ v)) = + (𝕜 ∙ v).subtypeL.comp (orthogonalProjectionOnto (𝕜 ∙ v)) = (1 / (‖v‖ : 𝕜) ^ 2) • .toSpanSingleton 𝕜 v ∘L InnerProductSpace.toDual 𝕜 E v := by ext w simp [ContinuousLinearMap.toSpanSingleton_apply, starProjection_singleton, ← mul_smul, @@ -230,7 +230,7 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteS /-- The orthogonal projection onto a vector in a real inner product space `E`, considered as a map from `E` to `E →L[ℝ] E`, is analytic away from 0. -/ theorem contDiffAt_orthogonalProjection_singleton {v₀ : E} (hv₀ : v₀ ≠ 0) : - ContDiffAt ℝ ω (fun v : E ↦ (ℝ ∙ v).subtypeL.comp (orthogonalProjection (ℝ ∙ v))) v₀ := by + ContDiffAt ℝ ω (fun v : E ↦ (ℝ ∙ v).subtypeL.comp (orthogonalProjectionOnto (ℝ ∙ v))) v₀ := by suffices ContDiffAt ℝ ω (fun v : E ↦ (1 / ‖v‖ ^ 2) • .toSpanSingleton ℝ v ∘L InnerProductSpace.toDual ℝ E v) v₀ by refine this.congr_of_eventuallyEq ?_ diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean index cd4a4489..4ad6ea37 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean @@ -90,7 +90,7 @@ theorem norm_crossProduct (u : E) (v : (ℝ ∙ u)ᗮ) : ‖u×₃v‖ = ‖u‖ simpa only [inner_crossProduct_apply, AddSubgroupClass.coe_norm, mul_assoc, Fin.prod_univ_succ, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_succ, Finset.univ_unique, Fin.default_eq_zero, Matrix.cons_val_fin_one, Finset.prod_const, - Finset.card_singleton, pow_one] using ω.volumeForm_apply_le ![u, v, u×₃v] + Finset.card_singleton, pow_one] using! ω.volumeForm_apply_le ![u, v, u×₃v] let K : Submodule ℝ E := Submodule.span ℝ ({u, ↑v} : Set E) have : Nontrivial Kᗮ := by apply Module.nontrivial_of_finrank_pos (R := ℝ) diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean index 5ce5fb46..714ca6a5 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean @@ -53,7 +53,7 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] --[Complet /-- The orthogonal projection to the complement of `span x`. -/ @[reducible] def projSpanOrthogonal (x : E) := - orthogonalProjection (Submodule.span ℝ ({x} : Set E))ᗮ + orthogonalProjectionOnto (Submodule.span ℝ ({x} : Set E))ᗮ @[inherit_doc] local notation "{." x "}ᗮ" => spanOrthogonal x @@ -67,7 +67,7 @@ theorem orthogonal_line_inf {u v : E} : {.u}ᗮ ⊓ {.v}ᗮ = {.(pr[v]ᗮ u : E) rw [span_singleton_le_iff_mem] · nth_rw 2 [← starProjection_add_starProjection_orthogonal (K := Δ v) u] exact add_mem (mem_sup_right <| coe_mem _) (mem_sup_left <| mem_span_singleton_self _) - · rw [projSpanOrthogonal, orthogonalProjection_orthogonal] + · rw [projSpanOrthogonal, orthogonalProjectionOnto_orthogonal] exact sub_mem (mem_sup_left <| mem_span_singleton_self _) (mem_sup_right <| coe_mem _) theorem orthogonal_line_inf_sup_line (u v : E) : {.u}ᗮ ⊓ {.v}ᗮ ⊔ Δ (pr[v]ᗮ u : E) = {.v}ᗮ := by @@ -76,13 +76,13 @@ theorem orthogonal_line_inf_sup_line (u v : E) : {.u}ᗮ ⊓ {.v}ᗮ ⊔ Δ (pr[ exact coe_mem _ theorem orthogonalProjection_eq_zero_of_mem {F : Submodule ℝ E} [CompleteSpace F] {x : E} - (h : x ∈ Fᗮ) : orthogonalProjection F x = 0 := by + (h : x ∈ Fᗮ) : orthogonalProjectionOnto F x = 0 := by refine Subtype.coe_injective (eq_starProjection_of_mem_of_inner_eq_zero F.zero_mem ?_) simp only [coe_zero, sub_zero] exact (mem_orthogonal' F x).mp h theorem inner_projection_self_eq_zero_iff {F : Submodule ℝ E} [CompleteSpace F] {x : E} : - ⟪x, orthogonalProjection F x⟫ = 0 ↔ x ∈ Fᗮ := by + ⟪x, orthogonalProjectionOnto F x⟫ = 0 ↔ x ∈ Fᗮ := by obtain ⟨y, hy, z, hz, rfl⟩ := F.exists_add_mem_mem_orthogonal x rw [inner_add_left, map_add, coe_add, inner_add_right, inner_add_right] suffices y = 0 ↔ y + z ∈ Fᗮ by @@ -156,15 +156,15 @@ def orthogonalProjectionOrthogonalLineIso {x₀ x : E} (h : ⟪x₀, x⟫ ≠ 0) ext dsimp rw [map_sub, map_smul, starProjection_apply, starProjection_apply, - orthogonalProjection_orthogonalComplement_singleton_eq_zero, coe_zero, + orthogonalProjectionOnto_orthogonalComplement_singleton_eq_zero, coe_zero, ← starProjection_apply, smul_zero, sub_zero, starProjection_eq_self_iff.mpr hy] continuous_toFun := (pr[x]ᗮ.comp (subtypeL {.x₀}ᗮ)).continuous continuous_invFun := by fun_prop } theorem orthogonalProjection_comp_coe (K : Submodule ℝ E) [CompleteSpace K] : - orthogonalProjection K ∘ ((↑) : K → E) = id := by + orthogonalProjectionOnto K ∘ ((↑) : K → E) = id := by ext1 x - exact orthogonalProjection_mem_subspace_eq_self x + exact orthogonalProjectionOnto_mem_subspace_eq_self x variable (E) @@ -212,8 +212,8 @@ theorem continuousAt_orthogonalProjection_orthogonal {x₀ : E} (hx₀ : x₀ ∃ δ > 0, ∀ y, ‖y - x₀‖ ≤ δ → ∀ x, ‖(⟪x₀, x⟫ / ⟪x₀, x₀⟫) • x₀ - (⟪y, x⟫ / ⟪y, y⟫) • y‖ ≤ ε * ‖x‖ by simpa only [ContinuousLinearMap.opNorm_le_iff (le_of_lt ε_pos), - orthogonalProjection_orthogonal_singleton, ContinuousLinearMap.coe_sub', - ContinuousLinearMap.coe_comp', coe_subtypeL, Submodule.coe_subtype, Pi.sub_apply, comp_apply, + orthogonalProjection_orthogonal_singleton, FunLike.coe_sub, + ContinuousLinearMap.coe_comp, coe_subtypeL, Submodule.coe_subtype, Pi.sub_apply, comp_apply, coe_mk, sub_sub_sub_cancel_left] let N : E → E := fun x ↦ ⟪x, x⟫⁻¹ • x have hNx₀ : 0 < ‖N x₀‖ := by diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean index a6f58e75..e365eec5 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean @@ -33,16 +33,16 @@ namespace Orientation and `t : ℝ` this endomorphism will be the rotation by the angle `t` about the axis spanned by `v`. -/ def rot (p : ℝ × E) : E →L[ℝ] E := - (ℝ ∙ p.2).subtypeL ∘L (orthogonalProjection (ℝ ∙ p.2) : E →L[ℝ] ℝ ∙ p.2) + + (ℝ ∙ p.2).subtypeL ∘L (orthogonalProjectionOnto (ℝ ∙ p.2) : E →L[ℝ] ℝ ∙ p.2) + Real.cos (p.1 * Real.pi) • - (ℝ ∙ p.2)ᗮ.subtypeL ∘L (orthogonalProjection (ℝ ∙ p.2)ᗮ : E →L[ℝ] (ℝ ∙ p.2)ᗮ) + + (ℝ ∙ p.2)ᗮ.subtypeL ∘L (orthogonalProjectionOnto (ℝ ∙ p.2)ᗮ : E →L[ℝ] (ℝ ∙ p.2)ᗮ) + Real.sin (p.1 * Real.pi) • LinearMap.toContinuousLinearMap (ω.crossProduct p.2) /-- Alternative form of the construction `rot`, convenient for the smoothness calculation. -/ def rotAux (p : ℝ × E) : E →L[ℝ] E := Real.cos (p.1 * Real.pi) • ContinuousLinearMap.id ℝ E + ((1 - Real.cos (p.1 * Real.pi)) • - (ℝ ∙ p.2).subtypeL ∘L (orthogonalProjection (ℝ ∙ p.2) : E →L[ℝ] ℝ ∙ p.2) + + (ℝ ∙ p.2).subtypeL ∘L (orthogonalProjectionOnto (ℝ ∙ p.2) : E →L[ℝ] ℝ ∙ p.2) + Real.sin (p.1 * Real.pi) • ω.crossProduct' p.2) theorem rot_eq_aux : ω.rot = ω.rotAux := by @@ -68,17 +68,17 @@ theorem rot_zero (v : E) : ω.rot (0, v) = ContinuousLinearMap.id ℝ E := by /-- The map `rot` sends `(1, v)` to a transformation which on `(ℝ ∙ v)ᗮ` acts as the negation. -/ theorem rot_one (v : E) {w : E} (hw : w ∈ (ℝ ∙ v)ᗮ) : ω.rot (1, v) w = -w := by - suffices (orthogonalProjection (Submodule.span ℝ {v}) w : E) + - -(orthogonalProjection (Submodule.span ℝ {v})ᗮ w) = -w by simpa [rot] - simp [starProjection_eq_self_iff.mpr hw, - orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hw] + suffices (orthogonalProjectionOnto (Submodule.span ℝ {v}) w : E) + + -(orthogonalProjectionOnto (Submodule.span ℝ {v})ᗮ w) = -w by simpa [rot] + simp [starProjection_eq_self_iff.mpr hw, orthogonalProjectionOnto_apply_of_mem_orthogonal hw] /-- The map `rot` sends `(v, t)` to a transformation fixing `v`. -/ @[simp] theorem rot_self (p : ℝ × E) : ω.rot p (no_index p.2) = p.2 := by - have H : orthogonalProjection (ℝ ∙ p.2) p.2 = p.2 := + have H : orthogonalProjectionOnto (ℝ ∙ p.2) p.2 = p.2 := starProjection_eq_self_iff.mpr (Submodule.mem_span_singleton_self p.2) - simp [rot, crossProduct_apply_self, orthogonalProjection_orthogonalComplement_singleton_eq_zero,H] + simp [rot, crossProduct_apply_self, + orthogonalProjectionOnto_orthogonalComplement_singleton_eq_zero, H] /-- The map `rot` sends `(t, v)` to a transformation preserving `span v`. -/ theorem rot_eq_of_mem_span (p : ℝ × E) {x : E} (hx : x ∈ ℝ ∙ p.2) : ω.rot p x = x := by @@ -87,10 +87,10 @@ theorem rot_eq_of_mem_span (p : ℝ × E) {x : E} (hx : x ∈ ℝ ∙ p.2) : ω. /-- The map `rot` sends `(v, t)` to a transformation preserving the subspace `(ℝ ∙ v)ᗮ`. -/ theorem inner_rot_apply_self (p : ℝ × E) (w : E) (hw : w ∈ (ℝ ∙ p.2)ᗮ) : ⟪ω.rot p w, no_index p.2⟫ = 0 := by - have H₁ : orthogonalProjection (ℝ ∙ p.2) w = 0 := - orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hw - have H₂ : (orthogonalProjection (ℝ ∙ p.2)ᗮ w : E) = w := - congr_arg (_ : (ℝ ∙ p.2)ᗮ → E) (orthogonalProjection_mem_subspace_eq_self ⟨w, hw⟩) + have H₁ : orthogonalProjectionOnto (ℝ ∙ p.2) w = 0 := + orthogonalProjectionOnto_apply_of_mem_orthogonal hw + have H₂ : (orthogonalProjectionOnto (ℝ ∙ p.2)ᗮ w : E) = w := + congr_arg (_ : (ℝ ∙ p.2)ᗮ → E) (orthogonalProjectionOnto_mem_subspace_eq_self ⟨w, hw⟩) have H₃ : ⟪w, p.2⟫ = 0 := by simpa only [real_inner_comm] using hw p.2 (Submodule.mem_span_singleton_self _) have H₄ : ⟪p.2×₃w, p.2⟫ = 0 := ω.inner_crossProduct_apply_self p.2 ⟨w, hw⟩ @@ -108,9 +108,7 @@ theorem isometry_on_rot (t : ℝ) (v : Metric.sphere (0 : E) 1) (w : (ℝ ∙ (v simp only [inner_add_left, inner_add_right, inner_smul_left, inner_smul_right, h1, h2, h3, RCLike.conj_to_real, Submodule.coe_inner] linear_combination ⟪(w : E), w⟫ * Real.cos_sq_add_sin_sq (t * Real.pi) - dsimp [rot] - simp [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero w.prop, - this] + simp [rot, orthogonalProjectionOnto_apply_of_mem_orthogonal w.prop, this] theorem isometry_rot (t : ℝ) (v : Metric.sphere (0 : E) 1) : Isometry (ω.rot (t, v)) := by rw [AddMonoidHomClass.isometry_iff_norm] @@ -121,8 +119,7 @@ theorem isometry_rot (t : ℝ) (v : Metric.sphere (0 : E) 1) : Isometry (ω.rot rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, sq, map_add, @norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero ℝ, @norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero ℝ] - · have hvw : ‖ω.rot (t, v) w‖ = ‖w‖ := ω.isometry_on_rot t v ⟨w, hw⟩ - simp [hvw] + · simp [ω.isometry_on_rot t v ⟨w, hw⟩] · simp [inner_smul_left, hw v (Submodule.mem_span_singleton_self _)] rw [real_inner_comm] simp [inner_smul_right, ω.inner_rot_apply_self (t, v) w hw] @@ -136,11 +133,11 @@ theorem injOn_rot_of_ne (t : ℝ) {x : E} (hx : x ≠ 0) : Set.InjOn (ω.rot (t, rw [← ContinuousLinearMap.coe_coe, ← LinearMap.disjoint_ker_iff_injOn, LinearMap.disjoint_ker] intro y hy' hy change - ↑((orthogonalProjection (span ℝ {x})) y) + - cos (t * Real.pi) • ↑((orthogonalProjection (span ℝ {x})ᗮ) y) + + ↑((orthogonalProjectionOnto (span ℝ {x})) y) + + cos (t * Real.pi) • ↑((orthogonalProjectionOnto (span ℝ {x})ᗮ) y) + Real.sin (t * Real.pi) • x×₃y = 0 at hy - rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hy', ← starProjection_apply, + rw [orthogonalProjectionOnto_apply_of_mem_orthogonal hy', ← starProjection_apply, starProjection_eq_self_iff.mpr hy', coe_zero, zero_add] at hy apply_fun fun x ↦ ‖x‖ ^ 2 at hy rw [pow_two, @norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero ℝ] at hy diff --git a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean index d9548d8f..bb5aa8c6 100644 --- a/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean +++ b/SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean @@ -56,15 +56,13 @@ theorem isBoundedLinearMap_coprod (𝕜 : Type*) [NontriviallyNormedField 𝕜] intros apply ContinuousLinearMap.coeFn_injective ext u - simp only [Prod.fst_add, Prod.snd_add, ContinuousLinearMap.coprod_apply, - ContinuousLinearMap.add_apply] + simp only [Prod.fst_add, Prod.snd_add, ContinuousLinearMap.coprod_apply, add_apply] ac_rfl map_smul := by intro r p apply ContinuousLinearMap.coeFn_injective ext x - simp only [Prod.smul_fst, Prod.smul_snd, ContinuousLinearMap.coprod_apply, - ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_add] + simp bound := by refine ⟨2, zero_lt_two, fun ⟨φ, ψ⟩ ↦ ?_⟩ apply ContinuousLinearMap.opNorm_le_bound _ (by positivity) diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean b/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean index 0e1d4eaf..9281516b 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean @@ -39,12 +39,12 @@ theorem nhds_hasBasis_balls_of_open_cov [I.Boundaryless] (x : M) {ι : Type*} {s · exact ((extChartAt I x).mapsTo.mono inter_subset_right Subset.rfl).image_subset · suffices m ⊆ s j by refine Subset.trans ?_ this - convert monotone_image (f := (extChartAt I x).symm) hr₁ + convert! monotone_image (f := (extChartAt I x).symm) hr₁ exact (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).symm exact inter_subset_left.trans inter_subset_left · suffices m ⊆ n by refine Subset.trans ?_ this - convert monotone_image (f := (extChartAt I x).symm) hr₁ + convert! monotone_image (f := (extChartAt I x).symm) hr₁ exact (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).symm exact inter_subset_left.trans inter_subset_right · rintro ⟨r, ⟨hr₀, hr₁, -⟩, hr₂⟩ diff --git a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean index 515a18a1..7d0a3de3 100644 --- a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean +++ b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean @@ -15,9 +15,9 @@ theorem fst_prod_zero_add_zero_prod_snd [ContinuousAdd M₁] [ContinuousAdd M₂ ContinuousLinearMap.id R₁ (M₁ × M₂) := by rw [ContinuousLinearMap.ext_iff] intro x - simp_rw [ContinuousLinearMap.add_apply, ContinuousLinearMap.id_apply, - ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', - ContinuousLinearMap.zero_apply, Prod.mk_add_mk, add_zero, zero_add] + simp_rw [add_apply, ContinuousLinearMap.id_apply, ContinuousLinearMap.prod_apply, + ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', + zero_apply, Prod.mk_add_mk, add_zero, zero_add] end ContinuousLinearMap diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean index 9ca2a0d4..4af67c28 100644 --- a/SphereEversion/ToMathlib/Topology/Paracompact.lean +++ b/SphereEversion/ToMathlib/Topology/Paracompact.lean @@ -24,7 +24,7 @@ theorem exists_countable_locallyFinite_cover {ι X : Type*} [TopologicalSpace X] have hC' : (⋃ n, C n) = univ := by refine Set.univ_subset_iff.mp fun x _ ↦ mem_iUnion.mpr ⟨K'.find x, ?_⟩ simpa only [K'.find_shiftr] using - diff_subset_diff_right interior_subset (K'.shiftr.mem_diff_shiftr_find x) + sdiff_subset_sdiff_right interior_subset (K'.shiftr.mem_sdiff_shiftr_find x) have hU : ∀ n, IsOpen (U n) := fun n ↦ isOpen_interior.sdiff <| IsCompact.isClosed <| K.isCompact _ have hU' : ∀ n, {m | (U m ∩ U n).Nonempty}.Finite := fun n ↦ by @@ -35,9 +35,9 @@ theorem exists_countable_locallyFinite_cover {ι X : Type*} [TopologicalSpace X] ⟨this hx₄ hx₁, this hx₂ hx₃⟩ intro a b ha hb by_contra hab - replace hab : b + 1 ≤ a := by simpa using hab + replace hab : b + 1 ≤ a := by lia exact Set.Nonempty.ne_empty (⟨x, interior_subset hb, ha⟩ : (K b.succ \ K a).Nonempty) - (Set.diff_eq_empty.mpr (K.subset hab)) + (Set.sdiff_eq_empty.mpr (K.subset hab)) have hU'' : ∀ n x, x ∈ C n → U n ∈ 𝓝 x := fun n x hx ↦ mem_nhds_iff.mpr ⟨U n, Subset.rfl, hU n, hCU n hx⟩ have : ∀ (n) (x : C n), ∃ i r, ↑x ∈ W i r ∧ B i r ⊆ U n ∧ p i r := fun n ⟨x, hx⟩ ↦ by diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean index dc53804c..f09fd795 100644 --- a/SphereEversion/ToMathlib/Topology/Path.lean +++ b/SphereEversion/ToMathlib/Topology/Path.lean @@ -121,7 +121,7 @@ theorem Continuous.path_strans {X Y : Type*} [UniformSpace X] · intro h have ht : t x = 0 := Subtype.ext h apply Filter.Tendsto.pathExtend - dsimp only; rw [(projIcc_surjective _).filter_map_top, extend_zero] + rw [(projIcc_surjective _).filter_map_top, extend_zero] exact tendsto_prod_top_iff.mpr (hγ0 ht) · rw [continuous_iff_continuousAt] intro x @@ -134,7 +134,7 @@ theorem Continuous.path_strans {X Y : Type*} [UniformSpace X] · intro h have ht : t x = 1 := Subtype.ext (sub_eq_zero.mp h).symm apply Filter.Tendsto.pathExtend - dsimp only; rw [(projIcc_surjective _).filter_map_top, extend_zero] + rw [(projIcc_surjective _).filter_map_top, extend_zero] exact tendsto_prod_top_iff.mpr (hγ'1 ht) · rintro x h; rw [h, sub_self, zero_div, extend_div_self, extend_zero] diff --git a/lake-manifest.json b/lake-manifest.json index 3485f270..a1959cd8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f", + "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", + "inputRev": "v4.31.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a456461b368b71d2accd95234832cd9c174b5437", + "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1", + "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,37 +55,37 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8", + "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.99", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "558915ae105bfd8074e22d597613d1961822adc2", + "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c", + "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "32dc18cde3684679f3c003de608743b57498c56f", + "rev": "fa08db58b30eb033edcdab331bba000827f9f785", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c", + "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.30.0", + "inputRev": "v4.31.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "SphereEversion", diff --git a/lakefile.toml b/lakefile.toml index 7a03b960..f2a95077 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -11,7 +11,6 @@ weak.linter.style.header = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.30.0" [[require]] name = "checkdecls" diff --git a/lean-toolchain b/lean-toolchain index 5a8f1613..133a3f7d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.30.0 \ No newline at end of file +leanprover/lean4:v4.31.0 \ No newline at end of file