diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index e92f1be3..663339b0 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -44,19 +44,21 @@ theorem mem_immersionRel_iff {σ : OneJetBundle I M I' M'} : σ ∈ immersionRel I M I' M' ↔ Injective (σ.2 : TangentSpace I _ →L[ℝ] TangentSpace I' _) := Iff.rfl +set_option backward.isDefEq.respectTransparency false in /-- A characterisation of the immersion relation in terms of a local chart. -/ theorem mem_immersionRel_iff' {σ σ' : OneJetBundle I M I' M'} (hσ' : σ' ∈ (ψJ σ).source) : σ' ∈ 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, - EquivLike.injective_comp] + EquivLike.injective_comp] exacts [hσ'.1.1, hσ'.1.2] theorem chartAt_image_immersionRel_eq {σ : OneJetBundle I M I' M'} : ψJ σ '' ((ψJ σ).source ∩ immersionRel I M I' M') = (ψJ σ).target ∩ {q : HJ | Injective q.2} := PartialEquiv.IsImage.image_eq fun _σ' hσ' ↦ (mem_immersionRel_iff' I I' hσ').symm +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 ?_ @@ -214,6 +216,7 @@ theorem formalEversionHolAtZero {t : ℝ} (ht : t < 1 / 4) : congr with y simp [smoothStep.of_lt ht] +set_option backward.isDefEq.respectTransparency false in theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) : (formalEversion E ω t).toOneJetSec.IsHolonomic := by intro x @@ -253,12 +256,6 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E F G : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] --- move to Analysis.Calculus.ContDiff.Basic, or so -theorem contDiff_prod_iff (f : E → F × G) (n : ℕ∞) : - ContDiff 𝕜 n f ↔ - ContDiff 𝕜 n (Prod.fst ∘ f) ∧ ContDiff 𝕜 n (Prod.snd ∘ f) := - ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩ - -- move to Analysis.Calculus.ContDiff.Defs, or so lemma ContDiff.inr (x : E) (n : ℕ∞) : ContDiff 𝕜 n fun p : F ↦ (⟨x, p⟩ : E × F) := by rw [contDiff_prod_iff] diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean index 7fbcd488..5c2a43d6 100644 --- a/SphereEversion/Global/Localisation.lean +++ b/SphereEversion/Global/Localisation.lean @@ -36,7 +36,7 @@ def OneJetSec.loc (F : OneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E') : JetSec E E' have : ContMDiffAt _ _ _ _ _ := F.contMDiff x₀ simp_rw +unfoldPartialApp [contMDiffAt_oneJetBundle, inTangentCoordinates, inCoordinates, TangentBundle.symmL_model_space, TangentBundle.continuousLinearMapAt_model_space, - ContinuousLinearMap.one_def, ContinuousLinearMap.comp_id, TangentSpace, + ContinuousLinearMap.one_def, TangentSpace, ContinuousLinearMap.id_comp] at this exact this.2.2.contDiffAt @@ -85,6 +85,7 @@ theorem JetSec.unloc_hol_at_iff (𝓕 : JetSec E E') (x : E) : rw [mfderiv_eq_fderiv] exact Iff.rfl +set_option backward.isDefEq.respectTransparency false in def HtpyJetSec.unloc (𝓕 : HtpyJetSec E E') : HtpyOneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E' where bs t := (𝓕 t).f ϕ t x := (𝓕 t x).2 diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 2a6adf9b..65073607 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -95,13 +95,11 @@ def OneJetSpace (p : M × M') : Type _ := ((ContMDiffMap.fst : C^∞⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) p →SL[σ] ((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) p -instance (p : M × M') : TopologicalSpace (OneJetSpace I I' p) := by - delta OneJetSpace - infer_instance +instance (p : M × M') : TopologicalSpace (OneJetSpace I I' p) := + inferInstanceAs <| TopologicalSpace (E →L[𝕜] E') -instance (p : M × M') : AddCommGroup (OneJetSpace I I' p) := by - delta OneJetSpace - infer_instance +instance (p : M × M') : AddCommGroup (OneJetSpace I I' p) := + inferInstanceAs <| AddCommGroup (E →L[𝕜] E') variable {I I'} @@ -148,34 +146,38 @@ section variable {M} (p : M × M') -instance (x : M × M') : Module 𝕜 (FJ¹MM' x) := by - delta OneJetSpace - infer_instance +instance (x : M × M') : Module 𝕜 (FJ¹MM' x) := + inferInstanceAs <| Module 𝕜 (E →L[𝕜] E') end +set_option backward.isDefEq.respectTransparency false in instance : TopologicalSpace J¹MM' := by delta OneJetSpace OneJetBundle infer_instance +set_option backward.isDefEq.respectTransparency false in instance : FiberBundle (E →L[𝕜] E') FJ¹MM' := by delta OneJetSpace infer_instance - +set_option backward.isDefEq.respectTransparency false in instance : VectorBundle 𝕜 (E →L[𝕜] E') FJ¹MM' := by delta OneJetSpace infer_instance +set_option backward.isDefEq.respectTransparency false in instance : ContMDiffVectorBundle ∞ (E →L[𝕜] E') (OneJetSpace I I' : M × M' → Type _) (I.prod I') := by delta OneJetSpace infer_instance +set_option backward.isDefEq.respectTransparency false in instance : ChartedSpace HJ J¹MM' := by delta OneJetSpace OneJetBundle infer_instance +set_option backward.isDefEq.respectTransparency false in instance : IsManifold ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ J¹MM' := by apply Bundle.TotalSpace.isManifold @@ -195,7 +197,7 @@ theorem oneJetBundle_trivializationAt (x₀ x : J¹MM') : inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀.proj.1 x.proj.1 x₀.proj.2 x.proj.2 x.2 := by delta OneJetSpace - rw [continuousLinearMap_trivializationAt, Trivialization.continuousLinearMap_apply] + erw [continuousLinearMap_trivializationAt, Trivialization.continuousLinearMap_apply] simp only [inCoordinates] congr 2 exact Trivialization.pullback_symmL ContMDiffMap.fst @@ -214,6 +216,7 @@ theorem trivializationAt_oneJetBundle_target (x₀ : M × M') : Set.univ := rfl +set_option backward.isDefEq.respectTransparency false in /-- Computing the value of a chart around `v` at point `v'` in `J¹(M, M')`. The last component equals the continuous linear map `v'.2`, composed on both sides by an appropriate coordinate change function. -/ @@ -226,6 +229,7 @@ theorem oneJetBundle_chartAt_apply (v v' : OneJetBundle I M I' M') : rw [FiberBundle.chartedSpace_chartAt_snd] exact oneJetBundle_trivializationAt v v' +set_option backward.isDefEq.respectTransparency false in /-- In `J¹(M, M')`, the source of a chart has a nice formula -/ theorem oneJetBundle_chart_source (x₀ : J¹MM') : (chartAt HJ x₀).source = @@ -298,6 +302,7 @@ lemma ContMDiffMap.snd_apply (x : M) (x' : M') : end +set_option backward.isDefEq.respectTransparency false in /-- In `J¹(M, M')`, the target of a chart has a nice formula -/ theorem oneJetBundle_chart_target (x₀ : J¹MM') : (chartAt HJ x₀).target = Prod.fst ⁻¹' (chartAt (ModelProd H H') x₀.proj).target := by @@ -325,6 +330,7 @@ theorem oneJetBundle_chart_target (x₀ : J¹MM') : section Maps +set_option backward.isDefEq.respectTransparency false in theorem contMDiff_oneJetBundle_proj : ContMDiff ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) (I.prod I') ∞ (π (E →L[𝕜] E') FJ¹MM') := by apply contMDiff_proj _ @@ -356,6 +362,7 @@ theorem oneJetBundle_mk_snd {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} : (OneJetBundle.mk x y f).2 = f := rfl +set_option backward.isDefEq.respectTransparency false in theorem contMDiffAt_oneJetBundle {f : N → J¹MM'} {x₀ : N} : ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f x₀ ↔ CMDiffAt ∞ (fun x ↦ (f x).1.1) x₀ ∧ @@ -464,7 +471,7 @@ theorem ContMDiff.oneJet_add {f : N → M} {g : N → M'} {ϕ ϕ' : ∀ x : N, O simp_rw +unfoldPartialApp [inTangentCoordinates, inCoordinates] conv => enter [4, x, 2] - rw [ContinuousLinearMap.add_comp] + erw [ContinuousLinearMap.add_comp] simp only [ContinuousLinearMap.comp_add] exact hϕ.2.2.add hϕ'.2.2 @@ -478,6 +485,7 @@ protected def OneJetBundle.map (f : M → N) (g : M' → N') variable {I' J'} +set_option backward.isDefEq.respectTransparency false in omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃] [IsManifold J' ∞ N'] [IsManifold J ∞ N] in @@ -533,6 +541,7 @@ theorem ContMDiffAt.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 backward.isDefEq.respectTransparency false in set_option linter.style.multiGoal false in omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃] @@ -637,6 +646,7 @@ variable (I I') -- note: this proof works for all vector bundles where we have proven -- `∀ p, chartAt _ p = f.toPartialEquiv` +set_option backward.isDefEq.respectTransparency false in /-- The canonical identification between the one-jet bundle to the model space and the product, as a homeomorphism -/ def oneJetBundleModelSpaceHomeomorph : OneJetBundle I H I' H' ≃ₜ 𝓜 := diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index a67cad4f..865d2633 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -102,6 +102,7 @@ of its base map at x. -/ def IsHolonomicAt (F : OneJetSec I M I' M') (x : M) : Prop := mfderiv% F.bs x = (F x).2 +set_option backward.isDefEq.respectTransparency false in /-- A section of J¹(M, M') is holonomic at (x : M) iff it coincides with the 1-jet extension of its base map at x. -/ theorem isHolonomicAt_iff {F : OneJetSec I M I' M'} {x : M} : @@ -265,7 +266,7 @@ theorem uncurry_ϕ' (S : FamilyOneJetSec I M I' M' IP P) (p : P × M) : convert mfderiv_comp p ((S.contMDiff_bs.comp (contMDiff_id.prodMk contMDiff_const)).mdifferentiable (by simp) p.1) (contMDiff_fst.mdifferentiable one_ne_zero p) - simp_rw [mfderiv_fst] + on_goal 1 => simp_rw [mfderiv_fst] rfl theorem isHolonomicAt_uncurry (S : FamilyOneJetSec I M I' M' IP P) {p : P × M} : diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index 79c0b8e1..034e20b3 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -87,7 +87,7 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'} have hup : ((0 : EP), u) ∈ p.π.ker := (h2pq u).trans hu erw [q.update_apply _ hu, ← Prod.zero_mk_add_zero_mk, map_add, p.update_ker_pi _ _ hup, ← Prod.smul_zero_mk, map_smul] - conv_lhs => rw [← sub_add_cancel (0, q.v) p.v] + conv_lhs => erw [← sub_add_cancel (0, q.v) p.v] erw [map_add, p.update_ker_pi _ _ hv, p.update_v, bundleSnd_eq] rfl erw [← preimage_vadd_neg, mem_preimage, mem_slice, R.mem_relativize] @@ -134,6 +134,7 @@ theorem RelMfld.Ample.relativize (hR : R.Ample) : (R.relativize IP P).Ample := b rw [relativize_slice q rfl] exact (hR q).vadd +set_option backward.isDefEq.respectTransparency false in theorem FamilyOneJetSec.uncurry_mem_relativize (S : FamilyOneJetSec I M I' M' IP P) {s : P} {x : M} : S.uncurry (s, x) ∈ R.relativize IP P ↔ S s x ∈ R := by simp_rw [RelMfld.relativize, mem_preimage, bundleSnd_eq, OneJetSec.coe_apply, mapLeft] @@ -150,7 +151,9 @@ theorem FamilyOneJetSec.uncurry_mem_relativize (S : FamilyOneJetSec I M I' M' IP erw [S.uncurry_ϕ', ContinuousLinearMap.comp_apply, ContinuousLinearMap.add_apply, ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ContinuousLinearMap.coe_fst', ContinuousLinearMap.comp_apply] - simp + simp only [uncurry_bs, bs_eq_coe_bs, add_eq_right] + -- adaptation note: the proof used to be done now! + exact ContinuousLinearMap.map_zero _ def FamilyFormalSol.uncurry (S : FamilyFormalSol IP P R) : FormalSol (R.relativize IP P) := by refine ⟨S.toFamilyOneJetSec.uncurry, ?_⟩ @@ -207,6 +210,7 @@ theorem FamilyOneJetSec.curry_ϕ' (S : FamilyOneJetSec (IP.prod I) (P × M) I' M rw [mfderiv_id, mfderiv_const] rfl +set_option backward.isDefEq.respectTransparency false in theorem FormalSol.eq_iff {F₁ F₂ : FormalSol R} {x : M} : F₁ x = F₂ x ↔ F₁.bs x = F₂.bs x ∧ F₁.ϕ x = by apply F₂.ϕ x := by simp [Bundle.TotalSpace.ext_iff, FormalSol.fst_eq, FormalSol.snd_eq] @@ -221,6 +225,7 @@ theorem FamilyOneJetSec.isHolonomicAt_curry (S : FamilyOneJetSec (IP.prod I) (P rw [id, hS] rfl +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 ⊢ @@ -237,6 +242,7 @@ theorem FamilyFormalSol.curry_ϕ' (S : FamilyFormalSol J N (R.relativize IP P)) (S.curry p).ϕ x = (S p.1).ϕ (p.2, x) ∘L ContinuousLinearMap.inr ℝ EP E := S.toFamilyOneJetSec.curry_ϕ' p x +set_option backward.isDefEq.respectTransparency false in theorem curry_eq_iff_eq_uncurry {𝓕 : FamilyFormalSol J N (R.relativize IP P)} {𝓕₀ : FamilyFormalSol IP P R} {t : N} {x : M} {s : P} (h : 𝓕 t (s, x) = 𝓕₀.uncurry (s, x)) : (𝓕.curry (t, s)) x = 𝓕₀ s x := by diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index 67b3cf2b..17091cad 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -68,6 +68,7 @@ variable {R : RelMfld I M I' M'} structure FormalSol (R : RelMfld I M I' M') extends OneJetSec I M I' M' where is_sol' : ∀ x : M, toOneJetSec x ∈ R +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 @@ -183,6 +184,7 @@ theorem mem_slice {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : Dua {w : TM' σ.1.2} : w ∈ R.slice σ p ↔ OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R := Iff.rfl +set_option backward.isDefEq.respectTransparency false in omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : DualPair <| TM σ.1.1} (x : E') : @@ -515,6 +517,7 @@ instance (y : Y) : NormedAddCommGroup (TY y) := by assumption instance (y : Y) : NormedSpace ℝ (TY y) := by assumption +set_option backward.isDefEq.respectTransparency false in omit [IsManifold IX ∞ X] [IsManifold IM ∞ M] [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in /-- Ampleness survives localization -/ @@ -558,6 +561,9 @@ def OneJetSec.localize (hF : range (F.bs ∘ φ) ⊆ range ψ) : OneJetSec IX X (F.contMDiff_bs.comp φ.contMDiff_to).contMDiffAt · exact .oneJet_comp IM φ (F.contMDiff_eta.comp φ.contMDiff_to) φ.contMDiff_to.oneJetExt +set_option maxHeartbeats 800000 in -- adaptation note: this is required since the bump +-- from version 4.28.0 to version 4.29.0-rc6 +set_option backward.isDefEq.respectTransparency false in theorem transfer_localize (hF : range (F.bs ∘ φ) ⊆ range ψ) (x : X) : φ.transfer ψ (F.localize φ ψ hF x) = F (φ x) := by rw [OneJetSec.coe_apply, OneJetSec.localize_bs, OneJetSec.localize_ϕ, @@ -570,7 +576,9 @@ theorem transfer_localize (hF : range (F.bs ∘ φ) ⊆ range ψ) (x : X) : -- continuous_linear_equiv.coe_coe, continuous_linear_equiv.apply_symm_apply] -- 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, + rw [← ψ.fderiv_coe] + rw [ContinuousLinearMap.comp_apply] + erw [ContinuousLinearEquiv.coe_coe, ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.apply_symm_apply] rfl @@ -583,6 +591,7 @@ theorem OneJetSec.localize_mem_iff (hF : range (F.bs ∘ φ) ⊆ range ψ) {x : F.localize φ ψ hF x ∈ R.localize φ ψ ↔ F (φ x) ∈ R := by rw [RelMfld.localize, mem_preimage, transfer_localize F φ ψ hF] +set_option backward.isDefEq.respectTransparency false in theorem isHolonomicAt_localize_iff (hF : range (F.bs ∘ φ) ⊆ range ψ) (x : X) : (F.localize φ ψ hF).IsHolonomicAt x ↔ F.IsHolonomicAt (φ x) := by have : @@ -604,6 +613,7 @@ theorem isHolonomicAt_localize_iff (hF : range (F.bs ∘ φ) ⊆ range ψ) (x : /-! ## From embeddings `X ↪ M` and `Y ↪ N` to `J¹(X, Y) ↪ J¹(M, N)` -/ -- very slow to elaborate :-( +set_option backward.isDefEq.respectTransparency false in @[simps] def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where toFun := φ.transfer ψ diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index c853e6ea..96d944bf 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -148,6 +148,7 @@ tangent space to `V` is canonically isomorphic to `V`. -/ def incl (v : J¹[𝕜, E, I, M, V] × V) : OneJetBundle I M 𝓘(𝕜, V) V := ⟨(v.1.1, v.2), v.1.2⟩ +set_option backward.isDefEq.respectTransparency false in theorem contMDiff_incl : ContMDiff ((I.prod 𝓘(𝕜, E →L[𝕜] V)).prod 𝓘(𝕜, V)) ((I.prod 𝓘(𝕜, V)).prod 𝓘(𝕜, E →L[𝕜] V)) ∞ (incl I M V) := by intro x₀ @@ -218,6 +219,7 @@ def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ∞ f) convert (contMDiff_incl I M V).comp (s.contMDiff.prodMk hf) ext : 1 <;> simp +set_option backward.isDefEq.respectTransparency false in def familyTwist (s : OneJetEuclSec I M V) (i : N × M → V →L[ℝ] V') (hi : ∀ x₀ : N × M, ContMDiffAt (J.prod I) 𝓘(ℝ, V →L[ℝ] V') ∞ i x₀) : FamilyOneJetEuclSec I M V' J N diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean index 998e1e25..08aba2c4 100644 --- a/SphereEversion/Indexing.lean +++ b/SphereEversion/Indexing.lean @@ -80,6 +80,7 @@ variable {n : ℕ} theorem IndexType.not_lt_zero (j : IndexType n) : ¬j < 0 := Nat.casesOn n Nat.not_lt_zero (fun _ ↦ Fin.not_lt_zero) j +set_option backward.isDefEq.respectTransparency false in theorem IndexType.zero_le (i : IndexType n) : 0 ≤ i := by cases n <;> dsimp at * <;> simp def IndexType.succ {N : ℕ} : IndexType N → IndexType N := Order.succ @@ -118,6 +119,7 @@ theorem IndexType.toNat_succ (i : IndexType n) (hi : ¬IsMax i) : theorem IndexType.not_isMax (n : IndexType 0) : ¬IsMax n := not_isMax_of_lt <| Nat.lt_succ_self n +set_option backward.isDefEq.respectTransparency false in @[elab_as_elim] theorem IndexType.induction_from {P : IndexType n → Prop} {i₀ : IndexType n} (h₀ : P i₀) (ih : ∀ i ≥ i₀, ¬IsMax i → P i → P i.succ) : ∀ i ≥ i₀, P i := by @@ -153,7 +155,7 @@ theorem IndexType.exists_by_induction {α : Type*} (P : IndexType n → α → P cases n with | zero => intro P Q h₀ ih - rcases exists_by_induction' P Q h₀ (by simpa using ih) with ⟨f, hf⟩ + rcases exists_by_induction' P Q h₀ (fun n a hn ↦ ih n a hn (not_isMax n)) with ⟨f, hf⟩ exact ⟨f, fun n ↦ ⟨(hf n).1, fun _ ↦ (hf n).2⟩⟩ | succ N => -- dsimp only [IndexType, IndexType.succ] diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index a36384b2..0dcc5230 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -342,7 +342,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ rintro ⟨t, x⟩ h' split_ifs with h · rfl - · push_neg at h + · push Not at h change (↿F') ((2 : ℝ) ^ (i.toNat + 1) * (t - T i.toNat), x) = _ rw [h', h₂F x t h.le] · have hp : ∀ᶠ p : ℝ × X in 𝓝 (t, x), p.1 ≤ T i.toNat := @@ -359,12 +359,11 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ simpa using ht' exact hp.mono fun q hq ↦ if_neg hq refine ⟨F'', ?_, ?_, ?_, ?_⟩ - · rintro p - by_cases ht : p.1 ≤ T i.toNat + · intro p + by_cases! ht : p.1 ≤ T i.toNat · rw [loc₁ _ ht] apply h₀F - · push_neg at ht - obtain ⟨t, x⟩ :=p + · obtain ⟨t, x⟩ :=p rw [loc₂ _ ht] refine ⟨h₀F' ((2 : ℝ) ^ (i.toNat + 1) * (t - T i.toNat)) x, ?_, ?_⟩ · rintro (rfl : t = 0) @@ -383,7 +382,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ congr rw [← mul_T_succ_sub i.toNat] gcongr - · push_neg + · push Not apply T_lt_succ · rintro j hj ⟨t, x⟩ (rfl : t = 1) replace h₁F' := eventually_nhdsSet_iUnion₂.mp h₁F' j hj @@ -408,7 +407,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ split_ifs with ht · rfl · rw [hUF' _ x hx] - push_neg at ht + push Not at ht rw [h₂F x _ ht.le] rcases inductive_construction PP₀ PP₁ PP₂ (U_fin.prod_left fun i ↦ Ici (T i.toNat)) ⟨fun p ↦ f₀ p.2, hPP₀, fun x t _ ↦ rfl⟩ ind' with diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean index a6cecac8..a4c0edff 100644 --- a/SphereEversion/Local/OneJet.lean +++ b/SphereEversion/Local/OneJet.lean @@ -271,7 +271,7 @@ theorem htpy_jet_sec_comp_aux {f g : ℝ → E → F} (hf : 𝒞 ∞ ↿f) (hg : prod_mem_nhds_iff.mpr ⟨Ioi_mem_nhds ht, univ_mem⟩ filter_upwards [this] with p hp obtain ⟨t, x⟩ := p - replace hp : ¬t ≤ 1 / 2 := by push_neg; exact (prodMk_mem_set_prod_eq.mp hp).1 + replace hp : ¬t ≤ 1 / 2 := by push Not; exact (prodMk_mem_set_prod_eq.mp hp).1 change ite (t ≤ 1 / 2) (f (smoothStep (2 * t)) x) (g (smoothStep (2 * t - 1)) x) = _ rw [if_neg hp] rfl diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean index d091bb62..35ca4025 100644 --- a/SphereEversion/Local/ParametricHPrinciple.lean +++ b/SphereEversion/Local/ParametricHPrinciple.lean @@ -57,6 +57,7 @@ def RelLoc.relativize (R : RelLoc E F) : RelLoc (P × E) F := variable {P} (R) +set_option backward.isDefEq.respectTransparency false in theorem RelLoc.mem_relativize (w : OneJet (P × E) F) : w ∈ R.relativize P ↔ (w.1.2, w.2.1, w.2.2 ∘L ContinuousLinearMap.inr ℝ P E) ∈ R := by simp_rw [RelLoc.relativize, mem_preimage, oneJetSnd_eq] @@ -145,6 +146,7 @@ theorem FamilyJetSec.uncurry_φ' (S : FamilyJetSec E F P) (p : P × E) : rfl open ContinuousLinearMap +set_option backward.isDefEq.respectTransparency false in 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, @@ -221,6 +223,7 @@ theorem FamilyJetSec.isHolonomicAt_curry (S : FamilyJetSec (P × E) F G) {t : G} rw [_root_.id, hS] rfl +set_option backward.isDefEq.respectTransparency false in theorem FamilyJetSec.curry_mem (S : FamilyJetSec (P × E) F G) {p : G × P} {x : E} (hR : ((p.2, x), S p.1 (p.2, x)) ∈ R.relativize P) : (x, S.curry p x) ∈ R := by unfold RelLoc.relativize at hR diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index 27800860..777a572a 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -496,8 +496,8 @@ theorem reparametrize_average : (γ.centeringDensity_continuous x).continuousOn have h₃ : Continuous fun s ↦ γ x (γ.reparametrize x s) := (γ.continuous x).comp (γ.reparametrize_smooth.continuous.uncurry_left x) - rw [← (γ.reparametrize x).symm.map_zero, ← (γ.reparametrize x).symm.map_one, ← - integral_comp_smul_deriv h₁ h₂ h₃] + rw [← (γ.reparametrize x).symm.map_zero, ← (γ.reparametrize x).symm.map_one, + ← integral_deriv_smul_comp h₁ h₂ h₃] simp only [comp_apply, EquivariantEquiv.apply_symm_apply, centeringDensity_average] end SmoothSurroundingFamily diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index d8be7593..92d3ee6b 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -192,7 +192,7 @@ theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} ( rw [AffineMap.image_convexHull] at hbε let t : Units ℝ := Units.mk0 ε (by linarith) refine ⟨AffineMap.homothety c (t : ℝ) '' b, hcs, ?_, ?_, hbε (convexHull_mono hb₁ hf)⟩ - · rwa [(AffineEquiv.homothetyUnitsMulHom c t).affineIndependent_set_of_eq_iff] + · erw [(AffineEquiv.homothetyUnitsMulHom c t).affineIndependent_set_of_eq_iff]; assumption · exact (AffineEquiv.homothetyUnitsMulHom c t).span_eq_top_iff.mp hb₄ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ diff --git a/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean b/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean index c15699ee..817ee571 100644 --- a/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean +++ b/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean @@ -36,6 +36,7 @@ variable {α : Type*} def ℤSubℝ : AddSubgroup ℝ := AddMonoidHom.range (Int.castAddHom ℝ) /-- The equivalence relation on `ℝ` corresponding to its partition as cosets of `ℤ`. -/ +@[implicit_reducible] def transOne : Setoid ℝ := QuotientAddGroup.leftRel ℤSubℝ /-- The proposition that a function on `ℝ` is periodic with period `1`. -/ diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean index 703fcfe2..91b9f329 100644 --- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean +++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean @@ -28,7 +28,7 @@ theorem finite_of_finprod_ne_one {M : Type*} {ι : Sort _} [CommMonoid M] {f : classical rw [finprod_def] at h contrapose h - rw [dif_neg h] + erw [dif_neg h] theorem support_finite_of_finsum_eq_of_neZero {M : Type*} {ι : Sort _} [AddCommMonoid M] {f : ι → M} {x : M} [NeZero x] (h : ∑ᶠ i, f i = x) : (support f).Finite := by @@ -112,7 +112,7 @@ theorem ReallyConvex.finsum_mem [Nontrivial 𝕜] [IsOrderedRing 𝕜] (hs : ReallyConvex 𝕜 s) {ι : Type*} {w : ι → 𝕜} {z : ι → E} (h₀ : ∀ i, 0 ≤ w i) (h₁ : ∑ᶠ i, w i = 1) (hz : ∀ i ∈ support w, z i ∈ s) : ∑ᶠ i, w i • z i ∈ s := by - rw [finsum_eq_sum_of_support_subset_of_finite _ _ (finite_support_of_finsum_eq_one h₁)] + rw [finsum_eq_sum_of_support_subset_of_finite _ _ (hasFiniteSupport_of_finsum_eq_one h₁)] swap; · exact support_smul_subset_left w z apply hs.sum_mem fun i _ ↦ h₀ i · rw [← finsum_eq_sum, h₁] @@ -146,7 +146,7 @@ theorem ReallyConvex.preimageₛₗ (f : E →ₛₗ[σ.toRingHom] E') {s : Set · simp_rw [preimage_empty, reallyConvex_empty] · simp_rw [preimage_univ, reallyConvex_univ] · refine Or.inr fun w hw h2w h3w ↦ ?_ - have h4w : (support w).Finite := finite_support_of_finsum_eq_one h3w + have h4w : (support w).Finite := hasFiniteSupport_of_finsum_eq_one h3w have : (support fun x ↦ w x • x).Finite := h4w.subset (support_smul_subset_left w id) simp_rw [mem_preimage, map_finsum f this, map_smulₛₗ f] apply hs.finsum_mem diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean index 4c628b39..7d16d1f0 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean @@ -56,7 +56,7 @@ theorem inner_crossProduct_apply (u v w : E) : ⟪u×₃v, w⟫ = ω.volumeForm Nat.succ_eq_add_one, Nat.reduceAdd, AlternatingMap.curryLeftLinearMap_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.llcomp_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply, LinearIsometryEquiv.coe_symm_toLinearEquiv] - rw [InnerProductSpace.toDual_symm_apply] + erw [InnerProductSpace.toDual_symm_apply] simp theorem inner_crossProduct_apply_self (u : E) (v : (ℝ ∙ u)ᗮ) : ⟪u×₃v, u⟫ = 0 := by diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index 63205e5a..eeb90b53 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -58,7 +58,7 @@ theorem reallyConvex_contMDiffAt (x : M) (n : ℕ∞) : classical rw [Nontrivial.reallyConvex_iff] rintro w _w_pos w_supp w_sum - have : (support w).Finite := finite_support_of_finsum_eq_one w_sum + have : (support w).Finite := hasFiniteSupport_of_finsum_eq_one w_sum set fin_supp := this.toFinset with H have : (support fun i : (𝓝 x).Germ F ↦ w i • i) ⊆ fin_supp := by rw [Set.Finite.coe_toFinset] @@ -121,8 +121,7 @@ theorem reallyConvex_contMDiffAtProd {x : M₁} (n : ℕ∞) : classical rw [Nontrivial.reallyConvex_iff] rintro w _w_pos w_supp w_sum - have : (support w).Finite := finite_support_of_finsum_eq_one w_sum - set fin_supp := this.toFinset with H + set fin_supp := (hasFiniteSupport_of_finsum_eq_one w_sum).toFinset with H have : (support fun i : (𝓝 x).Germ (M₂ → F) ↦ w i • i) ⊆ fin_supp := by rw [Set.Finite.coe_toFinset] exact support_smul_subset_left w id diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean index 64276ced..484d5884 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Metrizable.lean @@ -9,6 +9,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimension [ChartedSpace H M] /-- A metric defining the topology on a σ-compact T₂ real manifold. -/ +@[implicit_reducible] def manifoldMetric [T2Space M] [SigmaCompactSpace M] : MetricSpace M := letI := Manifold.metrizableSpace I M TopologicalSpace.metrizableSpaceMetric _ diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean index 9e16cdd2..57a7c003 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean @@ -161,10 +161,11 @@ variable [TopologicalSpace B'] [TopologicalSpace (TotalSpace F E)] [Nontrivially namespace Trivialization +set_option backward.isDefEq.respectTransparency false in theorem pullback_symmL (e : Trivialization F (π F E)) [e.IsLinear 𝕜] (x : B') : (e.pullback f).symmL 𝕜 x = e.symmL 𝕜 (f x) := by ext y - simp only [symmL_apply, pullback_symm] + simp only [Trivialization.symmL_apply, pullback_symm] rfl end Trivialization diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean index ffc4de3b..137f5287 100644 --- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean +++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean @@ -266,7 +266,7 @@ variable [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type theorem contDiff_parametric_primitive_of_contDiff {F : H → ℝ → E} {n : ℕ∞} (hF : ContDiff ℝ n ↿F) {s : H → ℝ} (hs : ContDiff ℝ n s) (a : ℝ) : ContDiff ℝ n fun x : H ↦ ∫ t in a..s x, F x t := by induction n using WithTop.recTopCoe - · rw [contDiff_infty] at * + · erw [contDiff_infty] at * exact fun n ↦ contDiff_parametric_primitive_of_contDiff' (hF n) (hs n) a · exact contDiff_parametric_primitive_of_contDiff' hF hs a diff --git a/lake-manifest.json b/lake-manifest.json index ba7dfe89..6e1a1e00 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", + "rev": "e4fca65b4fae96955832a3bc694aa89a064c3dc1", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", + "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", + "rev": "48d5698bc464786347c1b0d859b18f938420f060", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", + "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.87", + "inputRev": "v0.0.95", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", + "rev": "7152850e7b216a0d409701617721b6e469d34bf6", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", + "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", + "rev": "756e3321fd3b02a85ffda19fef789916223e578c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", + "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", + "inputRev": "v4.29.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "SphereEversion", diff --git a/lean-toolchain b/lean-toolchain index ea6ca7ff..d324cad1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0 \ No newline at end of file +leanprover/lean4:v4.29.0 \ No newline at end of file