diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index e92f1be3..af4fc2a2 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 ?_ @@ -168,7 +170,7 @@ variable (ω : Orientation ℝ E (Fin 3)) theorem smooth_bs : ContMDiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E) ∞ fun p : ℝ × (sphere (0 : E) 1) ↦ (1 - p.1) • (p.2 : E) + p.1 • -(p.2: E) := by - refine (ContMDiff.smul ?_ ?_).add (contMDiff_fst.smul ?_) + refine (ContMDiff.smul (I := 𝓘(ℝ)) ?_ ?_).add (contMDiff_fst.smul ?_) · exact (contDiff_const.sub contDiff_id).contMDiff.comp contMDiff_fst · exact (contMDiff_coe_sphere.of_le le_top).comp contMDiff_snd · exact (contDiff_neg.contMDiff.comp (contMDiff_coe_sphere.of_le le_top)).comp contMDiff_snd @@ -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..d1f7f928 100644 --- a/SphereEversion/Global/Localisation.lean +++ b/SphereEversion/Global/Localisation.lean @@ -36,8 +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.id_comp] at this + ContinuousLinearMap.one_def, TangentSpace] at this exact this.2.2.contDiffAt theorem OneJetSec.loc_hol_at_iff (F : OneJetSec 𝓘(ℝ, E) E 𝓘(ℝ, E') E') (x : E) : @@ -85,6 +84,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..e1d946fc 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 @@ -190,6 +192,7 @@ theorem oneJetBundle_proj_continuous : Continuous (π (E →L[𝕜] E') FJ¹MM') -- Porting note: removed next line -- attribute [simps] ContMDiffMap.fst ContMDiffMap.snd +set_option backward.isDefEq.respectTransparency false in theorem oneJetBundle_trivializationAt (x₀ x : J¹MM') : (trivializationAt (E →L[𝕜] E') (OneJetSpace I I') x₀.proj x).2 = inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀.proj.1 x.proj.1 x₀.proj.2 x.proj.2 @@ -214,6 +217,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 +230,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 +303,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 +331,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 +363,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₀ ∧ @@ -446,6 +454,7 @@ theorem ContMDiff.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} variable {I'} +set_option backward.isDefEq.respectTransparency false in open Trivialization in omit [IsManifold J ∞ N] in theorem ContMDiff.oneJet_add {f : N → M} {g : N → M'} {ϕ ϕ' : ∀ x : N, OneJetSpace I I' (f x, g x)} @@ -478,6 +487,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 +543,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 +648,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..a93be4ff 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -64,6 +64,7 @@ variable {σ : OneJetBundle (IP.prod I) (P × M) I' M'} #check (R.relativize IP P).slice σ p #check (R.slice (bundleSnd σ) q : Set <| TangentSpace I' σ.proj.2) -/ +set_option backward.isDefEq.respectTransparency false in omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold IP ∞ P] in theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'} {p : DualPair <| TangentSpace (IP.prod I) σ.1.1} (q : DualPair <| TangentSpace I σ.1.1.2) @@ -134,6 +135,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 +152,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 + -- adaptation note: in Lean 4.28, all this proof was just `simp` + simp only [uncurry_bs, 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 refine ⟨S.toFamilyOneJetSec.uncurry, ?_⟩ @@ -207,6 +211,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 +226,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 +243,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..0f270dbf 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 @@ -76,7 +77,6 @@ instance (R : RelMfld I M I' M') : FunLike (FormalSol R) M (OneJetBundle I M I' · exact congrArg Prod.snd (congrArg Bundle.TotalSpace.proj (congrFun h x)) · 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 where @@ -183,6 +183,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,8 +516,8 @@ instance (y : Y) : NormedAddCommGroup (TY y) := by assumption instance (y : Y) : NormedSpace ℝ (TY y) := by assumption -omit [IsManifold IX ∞ X] [IsManifold IM ∞ M] - [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in +set_option backward.isDefEq.respectTransparency false in +omit [IsManifold IX ∞ X] [IsManifold IM ∞ M] [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in /-- Ampleness survives localization -/ theorem RelMfld.Ample.localize (hR : R.Ample) : (R.localize φ ψ).Ample := by intro x p @@ -558,6 +559,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 +#adaptation_note /-- In Lean 4.28, this declaration was still reasonably fast -/ +set_option maxHeartbeats 600000 in +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,9 +574,16 @@ 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 ↦ ?_) + /- adaptation note: in Lean 4.28, this was erw [← ψ.fderiv_coe, ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.apply_symm_apply] + and much faster -/ + rw [← ψ.fderiv_coe, ContinuousLinearMap.comp_apply] + erw [ContinuousLinearEquiv.coe_coe (e := (φ.fderiv x).symm)] + rw [ContinuousLinearMap.comp_apply] + erw [ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.comp_apply, + ContinuousLinearEquiv.apply_symm_apply] rfl theorem OneJetSec.localize_bs_fun (hF : range (F.bs ∘ φ) ⊆ range ψ) : @@ -583,6 +594,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 : @@ -603,7 +615,8 @@ 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 :-( +-- 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..ee373030 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -10,8 +10,7 @@ import SphereEversion.Global.OneJetSec noncomputable section open Set Equiv Bundle ContinuousLinearMap - -open scoped Manifold Bundle Topology ContDiff +open scoped Manifold Topology ContDiff section ArbitraryField universe u v @@ -26,7 +25,6 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCo section Smoothness - notation "J¹[" 𝕜 ", " E ", " I ", " M ", " V "]" => TotalSpace (E →L[𝕜] V) (fun b ↦ (TangentSpace I : M → _) b →L[𝕜] (Bundle.Trivial M V) b) variable {I M V} @@ -127,7 +125,7 @@ theorem contMDiff_proj : ContMDiff ((I.prod 𝓘(𝕜, V)).prod 𝓘(𝕜, E → have : ContMDiffAt ((I.prod 𝓘(𝕜, V)).prod 𝓘(𝕜, E →L[𝕜] V)) _ ∞ id x₀ := contMDiffAt_id simp_rw +unfoldPartialApp [contMDiffAt_oneJetBundle, inTangentCoordinates, inCoordinates, TangentBundle.continuousLinearMapAt_model_space, ContinuousLinearMap.one_def, - TangentSpace, ContinuousLinearMap.id_comp] at this + TangentSpace] at this exact this.1.one_jet_eucl_bundle_mk this.2.2 variable {I M V} @@ -148,6 +146,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 +217,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/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index e5b74ce0..76d171f3 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -231,7 +231,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank 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] + ContinuousLinearMap.coe_comp', coe_subtypeL, Submodule.coe_subtype, comp_apply] 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 @@ -371,7 +371,7 @@ theorem locFormalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) {x : E} (hx : smoot simp only [mul_one, this, coe_orthogonalProjection_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_id'] + rw [fderiv_fun_neg, fderiv_fun_id] simp only [ContinuousLinearMap.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] diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index 27800860..b7adbedb 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -300,7 +300,7 @@ theorem localCenteringDensity_integral_eq_one (hy : y ∈ γ.localCenteringDensi ∫ s in (0 : ℝ)..1, γ.localCenteringDensity x y s = 1 := by let n := γ.localCenteringDensityMp x simp only [γ.localCenteringDensity_spec x, Fintype.sum_apply, Pi.smul_apply, smul_eq_mul] - rw [intervalIntegral.integral_finset_sum] + rw [intervalIntegral.integral_finsetSum] · have h : γ.approxSurroundingPointsAt x y n ∈ affineBases ι ℝ F := γ.approxSurroundingPointsAt_mem_affineBases x y hy simp_rw [← smul_eq_mul, intervalIntegral.integral_smul, deltaMollifier_integral_eq_one, @@ -317,7 +317,7 @@ theorem localCenteringDensity_average (hy : y ∈ γ.localCenteringDensityNhd x) let n := γ.localCenteringDensityMp x simp only [γ.localCenteringDensity_spec x, Fintype.sum_apply, Pi.smul_apply, smul_eq_mul, Finset.sum_smul] - rw [intervalIntegral.integral_finset_sum] + rw [intervalIntegral.integral_finsetSum] · simp_rw [mul_smul, intervalIntegral.integral_smul] change ∑ i, _ • γ.approxSurroundingPointsAt x y n i = _ have h : γ.approxSurroundingPointsAt x y n ∈ affineBases ι ℝ F := @@ -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..391e973f 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -173,6 +173,7 @@ theorem surrounded_iff_mem_interior_convexHull_aff_basis [FiniteDimensional ℝ (basis.sum_coord_apply_eq_one f), basis.affineCombination_coord_eq_self] --- `prop:surrounded_by_open` +set_option backward.isDefEq.respectTransparency false in theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} (hs : IsOpen s) (hsf : f ∈ convexHull ℝ s) : Surrounded f s := by rw [surrounded_iff_mem_interior_convexHull_aff_basis] @@ -192,7 +193,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] + · rw [(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..1e19c0b7 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] + rw [dif_neg (by exact 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..cd4a4489 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean @@ -2,8 +2,6 @@ Copyright (c) 2022 Heather Macbeth. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Heather Macbeth - -! This file was ported from Lean 3 source module to_mathlib.analysis.inner_product_space.cross_product -/ import Mathlib.Analysis.InnerProductSpace.Dual import Mathlib.Analysis.InnerProductSpace.Orientation @@ -51,6 +49,7 @@ local infixl:100 "×₃" => ω.crossProduct theorem crossProduct_apply_self (v : E) : v×₃v = 0 := by simp [crossProduct] +set_option backward.isDefEq.respectTransparency false in theorem inner_crossProduct_apply (u v w : E) : ⟪u×₃v, w⟫ = ω.volumeForm ![u, v, w] := by simp only [crossProduct, to_dual, LinearEquiv.trans_symm, LinearEquiv.symm_symm, Nat.succ_eq_add_one, Nat.reduceAdd, AlternatingMap.curryLeftLinearMap_apply, LinearMap.coe_comp, diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean index a6e353aa..5ce5fb46 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean @@ -213,7 +213,7 @@ theorem continuousAt_orthogonalProjection_orthogonal {x₀ : E} (hx₀ : 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, + 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/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..65d80026 100644 --- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean +++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean @@ -263,6 +263,7 @@ variable [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] -- Should we directly prove the version below? +set_option backward.isDefEq.respectTransparency false in 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 diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean index 1a2914de..9ca2a0d4 100644 --- a/SphereEversion/ToMathlib/Topology/Paracompact.lean +++ b/SphereEversion/ToMathlib/Topology/Paracompact.lean @@ -50,10 +50,10 @@ theorem exists_countable_locallyFinite_cover {ι X : Type*} [TopologicalSpace X] have hV₂ : ∀ n, C n ⊆ ⋃ x : C n, V n x := fun n x hx ↦ mem_iUnion.mpr ⟨⟨x, hx⟩, h₁ _ _⟩ choose f hf using fun n ↦ (hC n).elim_finite_subcover (V n) (hV₁ n) (hV₂ n) classical - let s : Set (ι × ℝ) := ⋃ n, (f n).image (Pi.prod (i n) (r n)) + let s : Set (ι × ℝ) := ⋃ n, (f n).image (Function.prod (i n) (r n)) refine ⟨s, countable_iUnion fun n ↦ Finset.countable_toSet _, fun z hz ↦ ?_, Set.univ_subset_iff.mp fun x _ ↦ ?_, fun x ↦ ?_⟩ - · simp only [Pi.prod, mem_iUnion, Finset.coe_image, mem_image, Finset.mem_coe, + · simp only [Function.prod, mem_iUnion, Finset.coe_image, mem_image, Finset.mem_coe, SetCoe.exists, s] at hz obtain ⟨n, x, hx, -, rfl⟩ := hz apply h₃ @@ -61,9 +61,9 @@ theorem exists_countable_locallyFinite_cover {ι X : Type*} [TopologicalSpace X] specialize hf n hn simp only [iUnion_coe_set, mem_iUnion, exists_prop] at hf obtain ⟨y, hy₁, hy₂, hy₃⟩ := hf - simp only [Pi.prod, mem_iUnion, Finset.mem_coe, Finset.mem_image, exists_prop, SetCoe.exists, - iUnion_exists, exists_and_right, Prod.exists, Prod.mk_inj, s] - exact ⟨i n ⟨y, hy₁⟩, r n ⟨y, hy₁⟩, ⟨n, y, hy₁, hy₂, rfl, rfl⟩, hy₃⟩ + simp only [mem_iUnion, Finset.mem_coe, Finset.mem_image, exists_prop, SetCoe.exists, + iUnion_exists, exists_and_right, Prod.exists, s] + exact ⟨i n ⟨y, hy₁⟩, r n ⟨y, hy₁⟩, ⟨n, y, hy₁, hy₂, rfl⟩, hy₃⟩ · obtain ⟨n, hn⟩ := iUnion_eq_univ_iff.mp hC' x refine ⟨U n, hU'' n x hn, ?_⟩ let P : ι × ℝ → Prop := fun z ↦ ((↿B) (z : ι × ℝ) ∩ U n).Nonempty @@ -72,7 +72,7 @@ theorem exists_countable_locallyFinite_cover {ι X : Type*} [TopologicalSpace X] refine (hU' n).iUnion (fun m _ ↦ Set.toFinite _) fun m hm ↦ ?_ rw [Set.eq_empty_iff_forall_notMem] intro z - simp only [Pi.prod, Finset.coe_image, mem_inter_iff, mem_image, Finset.mem_coe, SetCoe.exists, + simp only [Finset.coe_image, mem_inter_iff, mem_image, Finset.mem_coe, SetCoe.exists, mem_setOf_eq, not_and, exists₂_imp, and_imp] rintro x hx₁ - rfl rw [Set.not_nonempty_iff_eq_empty] diff --git a/lake-manifest.json b/lake-manifest.json index ba7dfe89..3485f270 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,4 +1,4 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/PatrickMassot/checkdecls.git", @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", + "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", + "rev": "a456461b368b71d2accd95234832cd9c174b5437", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", + "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,37 +55,37 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", + "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.87", + "inputRev": "v0.0.99", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", + "rev": "558915ae105bfd8074e22d597613d1961822adc2", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", + "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", + "rev": "32dc18cde3684679f3c003de608743b57498c56f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,11 +95,12 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", + "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", + "inputRev": "v4.30.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "SphereEversion", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index a81f4756..7a03b960 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,11 +6,12 @@ pp.unicode.fun = true autoImplicit = false relaxedAutoImplicit = false linter.mathlibStandardSet = true -linter.flexible = true +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 ea6ca7ff..5a8f1613 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0 \ No newline at end of file +leanprover/lean4:v4.30.0 \ No newline at end of file