From 597d3995700cb27213c3d2b7e9ecfa185adefaa1 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 26 Oct 2025 21:06:36 +0100 Subject: [PATCH 1/4] wip: use my elaborators branch, temporarily --- lake-manifest.json | 28 ++++++++++++++-------------- lakefile.toml | 3 ++- lean-toolchain | 2 +- 3 files changed, 17 insertions(+), 16 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 8d0aa48c..632cc44c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -11,21 +11,21 @@ "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4", + {"url": "https://github.com/grunweg/mathlib4.git", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "7c64d37d340c4fad44f930c9da90d2dae284bb8b", + "scope": "", + "rev": "d4a0bdb55c93112e3bdea8e86864379701317dbd", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "diffgeo-use-custom-elaborators", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b949552f6ca8e223f424b3e3b33f74185bbf1179", + "rev": "8864a73bf79aad549e34eff972c606343935106d", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d768126816be17600904726ca7976b185786e6b9", + "rev": "451499ea6e97cee4c8979b507a9af5581a849161", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "556caed0eadb7901e068131d1be208dd907d07a2", + "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.74", + "inputRev": "v0.0.77", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50", + "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2676cb5599c12c434daac781e2cea44e8105fc41", + "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee", + "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da", + "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.25.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "SphereEversion", diff --git a/lakefile.toml b/lakefile.toml index ba83c495..c289967f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -9,7 +9,8 @@ linter.mathlibStandardSet = true [[require]] name = "mathlib" -scope = "leanprover-community" +git = "https://github.com/grunweg/mathlib4.git" +rev = "diffgeo-use-custom-elaborators" [[require]] name = "checkdecls" diff --git a/lean-toolchain b/lean-toolchain index 58ae2451..137937a3 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.24.0 \ No newline at end of file +leanprover/lean4:v4.25.0-rc2 \ No newline at end of file From 50d75b1cf9a515ed5d28558a725aadbd33c409cb Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 26 Oct 2025 21:44:37 +0100 Subject: [PATCH 2/4] Use the elaborator more --- SphereEversion/Global/OneJetBundle.lean | 40 ++++++++----------- .../Global/ParametricityForFree.lean | 7 +--- 2 files changed, 18 insertions(+), 29 deletions(-) diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 5c9bda64..aa86ff70 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -331,12 +331,12 @@ theorem contMDiff_oneJetBundle_proj : theorem ContMDiff.oneJetBundle_proj {f : N โ†’ JยนMM'} (hf : ContMDiff J ((I.prod I').prod ๐“˜(๐•œ, E โ†’L[๐•œ] E')) โˆž f) : - ContMDiff J (I.prod I') โˆž fun x โ†ฆ (f x).1 := + CMDiff โˆž fun x โ†ฆ (f x).1 := contMDiff_oneJetBundle_proj.comp hf theorem ContMDiffAt.oneJetBundle_proj {f : N โ†’ JยนMM'} {xโ‚€ : N} (hf : ContMDiffAt J ((I.prod I').prod ๐“˜(๐•œ, E โ†’L[๐•œ] E')) โˆž f xโ‚€) : - ContMDiffAt J (I.prod I') โˆž (fun x โ†ฆ (f x).1) xโ‚€ := + CMDiffAt โˆž (fun x โ†ฆ (f x).1) xโ‚€ := (contMDiff_oneJetBundle_proj _).comp xโ‚€ hf /-- The constructor of `OneJetBundle`, in case `Sigma.mk` will not give the right type. -/ @@ -360,9 +360,8 @@ 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โ‚€ โˆง CMDiffAt โˆž (fun x โ†ฆ (f x).1.2) xโ‚€ โˆง - ContMDiffAt J ๐“˜(๐•œ, E โ†’L[๐•œ] E') โˆž - (inTangentCoordinates I I' (fun x โ†ฆ (f x).1.1) (fun x โ†ฆ (f x).1.2) (fun x โ†ฆ (f x).2) - xโ‚€) xโ‚€ := by + CMDiffAt โˆž (inTangentCoordinates I I' (fun x โ†ฆ (f x).1.1) + (fun x โ†ฆ (f x).1.2) (fun x โ†ฆ (f x).2) xโ‚€) xโ‚€ := by simp_rw [Bundle.contMDiffAt_totalSpace, contMDiffAt_prod_iff, and_assoc, oneJetBundle_trivializationAt] rfl @@ -370,13 +369,12 @@ theorem contMDiffAt_oneJetBundle {f : N โ†’ JยนMM'} {xโ‚€ : N} : theorem contMDiffAt_oneJetBundle_mk {f : N โ†’ M} {g : N โ†’ M'} {ฯ• : N โ†’ E โ†’L[๐•œ] E'} {xโ‚€ : N} : ContMDiffAt J ((I.prod I').prod ๐“˜(๐•œ, E โ†’L[๐•œ] E')) โˆž (fun x โ†ฆ OneJetBundle.mk (f x) (g x) (ฯ• x) : N โ†’ JยนMM') xโ‚€ โ†” - CMDiffAt โˆž f xโ‚€ โˆง CMDiffAt โˆž g xโ‚€ โˆง - ContMDiffAt J ๐“˜(๐•œ, E โ†’L[๐•œ] E') โˆž (inTangentCoordinates I I' f g ฯ• xโ‚€) xโ‚€ := + CMDiffAt โˆž f xโ‚€ โˆง CMDiffAt โˆž g xโ‚€ โˆง CMDiffAt โˆž (inTangentCoordinates I I' f g ฯ• xโ‚€) xโ‚€ := contMDiffAt_oneJetBundle theorem ContMDiffAt.oneJetBundle_mk {f : N โ†’ M} {g : N โ†’ M'} {ฯ• : N โ†’ E โ†’L[๐•œ] E'} {xโ‚€ : N} (hf : CMDiffAt โˆž f xโ‚€) (hg : CMDiffAt โˆž g xโ‚€) - (hฯ• : ContMDiffAt J ๐“˜(๐•œ, E โ†’L[๐•œ] E') โˆž (inTangentCoordinates I I' f g ฯ• xโ‚€) xโ‚€) : + (hฯ• : CMDiffAt โˆž (inTangentCoordinates I I' f g ฯ• xโ‚€) xโ‚€) : ContMDiffAt J ((I.prod I').prod ๐“˜(๐•œ, E โ†’L[๐•œ] E')) โˆž (fun x โ†ฆ OneJetBundle.mk (f x) (g x) (ฯ• x) : N โ†’ JยนMM') xโ‚€ := contMDiffAt_oneJetBundle.mpr โŸจhf, hg, hฯ•โŸฉ @@ -414,9 +412,9 @@ theorem ContinuousAt.inTangentCoordinates_comp {f : N โ†’ M} {g : N โ†’ M'} {h : theorem ContMDiffAt.clm_comp_inTangentCoordinates {f : N โ†’ M} {g : N โ†’ M'} {h : N โ†’ N'} {ฯ•' : N โ†’ E' โ†’L[๐•œ] F'} {ฯ• : N โ†’ E โ†’L[๐•œ] E'} {n : N} (hg : ContinuousAt g n) - (hฯ•' : ContMDiffAt J ๐“˜(๐•œ, E' โ†’L[๐•œ] F') โˆž (inTangentCoordinates I' J' g h ฯ•' n) n) - (hฯ• : ContMDiffAt J ๐“˜(๐•œ, E โ†’L[๐•œ] E') โˆž (inTangentCoordinates I I' f g ฯ• n) n) : - ContMDiffAt J ๐“˜(๐•œ, E โ†’L[๐•œ] F') โˆž (inTangentCoordinates I J' f h (fun n โ†ฆ ฯ•' n โˆ˜L ฯ• n) n) n := + (hฯ•' : CMDiffAt โˆž (inTangentCoordinates I' J' g h ฯ•' n) n) + (hฯ• : CMDiffAt โˆž (inTangentCoordinates I I' f g ฯ• n) n) : + CMDiffAt โˆž (inTangentCoordinates I J' f h (fun n โ†ฆ ฯ•' n โˆ˜L ฯ• n) n) n := (hฯ•'.clm_comp hฯ•).congr_of_eventuallyEq hg.inTangentCoordinates_comp variable (I') @@ -509,13 +507,10 @@ theorem OneJetBundle.map_id (x : JยนMM') : theorem ContMDiffAt.oneJetBundle_map {f : M'' โ†’ M โ†’ N} {g : M'' โ†’ M' โ†’ N'} {xโ‚€ : M''} {Dfinv : โˆ€ (z : M'') (x : M), TangentSpace J (f z x) โ†’L[๐•œ] TangentSpace I x} {k : M'' โ†’ JยนMM'} - (hf : ContMDiffAt (I''.prod I) J โˆž f.uncurry (xโ‚€, (k xโ‚€).1.1)) - (hg : ContMDiffAt (I''.prod I') J' โˆž g.uncurry (xโ‚€, (k xโ‚€).1.2)) - (hDfinv : - ContMDiffAt I'' ๐“˜(๐•œ, F โ†’L[๐•œ] E) โˆž - (inTangentCoordinates J I (fun x โ†ฆ f x (k x).1.1) (fun x โ†ฆ (k x).1.1) - (fun x โ†ฆ Dfinv x (k x).1.1) xโ‚€) - xโ‚€) + (hf : CMDiffAt โˆž f.uncurry (xโ‚€, (k xโ‚€).1.1)) + (hg : CMDiffAt โˆž g.uncurry (xโ‚€, (k xโ‚€).1.2)) + (hDfinv : CMDiffAt โˆž (inTangentCoordinates J I (fun x โ†ฆ f x (k x).1.1) (fun x โ†ฆ (k x).1.1) + (fun x โ†ฆ Dfinv x (k x).1.1) xโ‚€) xโ‚€) (hk : ContMDiffAt I'' ((I.prod I').prod ๐“˜(๐•œ, E โ†’L[๐•œ] E')) โˆž k xโ‚€) : ContMDiffAt I'' ((J.prod J').prod ๐“˜(๐•œ, F โ†’L[๐•œ] F')) โˆž (fun z โ†ฆ OneJetBundle.map I' J' (f z) (g z) (Dfinv z) (k z)) xโ‚€ := by @@ -544,12 +539,9 @@ theorem mapLeft_eq_map (f : M โ†’ N) (Dfinv : โˆ€ x : M, TangentSpace J (f x) theorem ContMDiffAt.mapLeft {f : N' โ†’ M โ†’ N} {xโ‚€ : N'} {Dfinv : โˆ€ (z : N') (x : M), TangentSpace J (f z x) โ†’L[๐•œ] TangentSpace I x} {g : N' โ†’ JยนMM'} - (hf : ContMDiffAt (J'.prod I) J โˆž f.uncurry (xโ‚€, (g xโ‚€).1.1)) - (hDfinv : - ContMDiffAt J' ๐“˜(๐•œ, F โ†’L[๐•œ] E) โˆž - (inTangentCoordinates J I (fun x โ†ฆ f x (g x).1.1) (fun x โ†ฆ (g x).1.1) - (fun x โ†ฆ Dfinv x (g x).1.1) xโ‚€) - xโ‚€) + (hf : CMDiffAt โˆž f.uncurry (xโ‚€, (g xโ‚€).1.1)) + (hDfinv : CMDiffAt โˆž (inTangentCoordinates J I (fun x โ†ฆ f x (g x).1.1) (fun x โ†ฆ (g x).1.1) + (fun x โ†ฆ Dfinv x (g x).1.1) xโ‚€) xโ‚€) (hg : ContMDiffAt J' ((I.prod I').prod ๐“˜(๐•œ, E โ†’L[๐•œ] E')) โˆž g xโ‚€) : ContMDiffAt J' ((J.prod I').prod ๐“˜(๐•œ, F โ†’L[๐•œ] E')) โˆž (fun z โ†ฆ mapLeft (f z) (Dfinv z) (g z)) xโ‚€ := by diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index 66513de0..e9c4e727 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -171,16 +171,13 @@ def FamilyOneJetSec.curry (S : FamilyOneJetSec (IP.prod I) (P ร— M) I' M' J N) : smooth' := by rintro โŸจโŸจt, sโŸฉ, xโŸฉ refine contMDiffAt_snd.oneJetBundle_mk (S.smooth_bs.comp contMDiff_prod_assoc _) ?_ - have h1 : - ContMDiffAt ((J.prod IP).prod I) ๐“˜(โ„, EP ร— E โ†’L[โ„] E') โˆž - (inTangentCoordinates (IP.prod I) I' (fun p : (N ร— P) ร— M โ†ฆ (p.1.2, p.2)) + have h1 : CMDiffAt โˆž (inTangentCoordinates (IP.prod I) I' (fun p : (N ร— P) ร— M โ†ฆ (p.1.2, p.2)) (fun p : (N ร— P) ร— M โ†ฆ (S p.1.1).bs (p.1.2, p.2)) (fun p : (N ร— P) ร— M โ†ฆ (S p.1.1).ฯ• (p.1.2, p.2)) ((t, s), x)) ((t, s), x) := by apply (contMDiffAt_oneJetBundle.mp <| ContMDiffAt.comp ((t, s), x) (S.smooth (t, (s, x))) (contMDiff_prod_assoc ((t, s), x))).2.2 - have h2 : - ContMDiffAt ((J.prod IP).prod I) ๐“˜(โ„, E โ†’L[โ„] EP ร— E) โˆž + have h2 : CMDiffAt โˆž (inTangentCoordinates I (IP.prod I) Prod.snd (fun p : (N ร— P) ร— M โ†ฆ (p.1.2, p.2)) (fun p : (N ร— P) ร— M โ†ฆ mfderiv I (IP.prod I) (fun x : M โ†ฆ (p.1.2, x)) p.2) ((t, s), x)) ((t, s), x) := by From ea701ce86f439516765ca49d9032cff956c464a6 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 26 Oct 2025 21:52:26 +0100 Subject: [PATCH 3/4] More --- SphereEversion/Global/Gromov.lean | 6 ++---- SphereEversion/Global/Immersion.lean | 5 ++--- SphereEversion/Global/OneJetSec.lean | 2 +- SphereEversion/Global/Relation.lean | 7 +++---- SphereEversion/Global/SmoothEmbedding.lean | 4 ++-- SphereEversion/Global/TwistOneJetSec.lean | 13 ++++++------- .../ToMathlib/Geometry/Manifold/MiscManifold.lean | 12 ++++-------- 7 files changed, 20 insertions(+), 29 deletions(-) diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean index f0b3af6e..d7dc7d77 100644 --- a/SphereEversion/Global/Gromov.lean +++ b/SphereEversion/Global/Gromov.lean @@ -67,10 +67,8 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R rintro a b โŸจt, xโŸฉ f h change ContMDiffAt _ _ _ (f โˆ˜ fun p : โ„ ร— M โ†ฆ (a * p.1 + b, p.2)) (t, x) change ContMDiffAt _ _ _ f ((fun p : โ„ ร— M โ†ฆ (a * p.1 + b, p.2)) (t, x)) at h - have : - ContMDiffAt (๐“˜(โ„, โ„).prod IM) (๐“˜(โ„, โ„).prod IM) โˆž (fun p : โ„ ร— M โ†ฆ (a * p.1 + b, p.2)) - (t, x) := - haveI hโ‚ : ContMDiffAt ๐“˜(โ„, โ„) ๐“˜(โ„, โ„) โˆž (fun t โ†ฆ a * t + b) t := + have : CMDiffAt โˆž (fun p : โ„ ร— M โ†ฆ (a * p.1 + b, p.2)) (t, x) := + haveI hโ‚ : CMDiffAt โˆž (fun t โ†ฆ a * t + b) t := contMDiffAt_iff_contDiffAt.mpr (((contDiffAt_id : ContDiffAt โ„ โˆž id t).const_smul a).add contDiffAt_const) hโ‚.prodMap contMDiffAt_id diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 30c4c3ee..266501b0 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -286,14 +286,13 @@ variable {๐•œ : Type*} [NontriviallyNormedField ๐•œ] {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] -- move to Mathlib.Geometry.Manifold.ContMDiff.Product -lemma ContMDiff.prod_left {n : โ„•โˆž} (x : M) : - ContMDiff I' (I.prod I') n fun p : M' โ†ฆ (โŸจx, pโŸฉ : M ร— M') := by +lemma ContMDiff.prod_left {n : โ„•โˆž} (x : M) : CMDiff n fun p : M' โ†ฆ (โŸจx, pโŸฉ : M ร— M') := by rw [contMDiff_prod_iff] exact โŸจcontMDiff_const, contMDiff_idโŸฉ -- move to Mathlib.Geometry.Manifold.ContMDiff.Product theorem ContMDiff.uncurry_left {n : โ„•โˆž} {f : M โ†’ M' โ†’ P} - (hf : ContMDiff (I.prod I') IP n โ†ฟf) (x : M) : CMDiff n (f x) := by + (hf : CMDiff n โ†ฟf) (x : M) : CMDiff n (f x) := by have : f x = (uncurry f) โˆ˜ fun p : M' โ†ฆ โŸจx, pโŸฉ := by ext; simp -- or just `apply hf.comp (ContMDiff.prod_left I I' x)` rw [this]; exact hf.comp (ContMDiff.prod_left I I' x) diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index 66c9876e..2b098313 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -222,7 +222,7 @@ protected theorem smooth (S : FamilyOneJetSec I M I' M' J N) : S.smooth' theorem smooth_bs (S : FamilyOneJetSec I M I' M' J N) : - ContMDiff (J.prod I) I' โˆž fun p : N ร— M โ†ฆ S.bs p.1 p.2 := + CMDiff โˆž fun p : N ร— M โ†ฆ S.bs p.1 p.2 := contMDiff_oneJetBundle_proj.snd.comp S.smooth theorem smooth_coe_bs (S : FamilyOneJetSec I M I' M' J N) {p : N} : CMDiff โˆž (S.bs p) := diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index 3e8b9d66..77803387 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -383,10 +383,9 @@ family of formal solutions. -/ theorem RelMfld.SatisfiesHPrincipleWith.bs {R : RelMfld I M IX X} {C : Set (P ร— M)} {ฮต : M โ†’ โ„} (h : R.SatisfiesHPrincipleWith IP C ฮต) (๐“•โ‚€ : FamilyFormalSol IP P R) (h2 : โˆ€แถ  p : P ร— M near C, (๐“•โ‚€ p.1).toOneJetSec.IsHolonomicAt p.2) : - โˆƒ f : P โ†’ M โ†’ X, - (ContMDiff (IP.prod I) IX โˆž <| uncurry f) โˆง - (โˆ€แถ  p : P ร— M near C, f p.1 p.2 = ๐“•โ‚€.bs p.1 p.2) โˆง - (โˆ€ p m, dist (f p m) ((๐“•โ‚€ p).bs m) โ‰ค ฮต m) โˆง โˆ€ p m, oneJetExt I IX (f p) m โˆˆ R := by + โˆƒ f : P โ†’ M โ†’ X, (CMDiff โˆž (uncurry f)) โˆง + (โˆ€แถ  p : P ร— M near C, f p.1 p.2 = ๐“•โ‚€.bs p.1 p.2) โˆง + (โˆ€ p m, dist (f p m) ((๐“•โ‚€ p).bs m) โ‰ค ฮต m) โˆง โˆ€ p m, oneJetExt I IX (f p) m โˆˆ R := by rcases h ๐“•โ‚€ h2 with โŸจ๐“•, _, hโ‚‚, hโ‚ƒ, hโ‚„โŸฉ refine โŸจfun s โ†ฆ (๐“• (1, s)).bs, ?_, ?_, ?_, ?_โŸฉ ยท let j : C^โˆžโŸฎIP, P; ๐“˜(โ„, โ„).prod IP, โ„ ร— PโŸฏ := diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index d455f2bb..73f73f53 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -424,8 +424,8 @@ open Function /-- This is lemma `lem:smooth_updating` in the blueprint. -/ theorem smooth_update (f : M' โ†’ M โ†’ N) (g : M' โ†’ X โ†’ Y) {k : M' โ†’ M} {K : Set X} - (hK : IsClosed (ฯ† '' K)) (hf : ContMDiff (IM'.prod IM) IN โˆž (uncurry f)) - (hg : ContMDiff (IM'.prod IX) IY โˆž (uncurry g)) (hk : CMDiff โˆž k) + (hK : IsClosed (ฯ† '' K)) + (hf : CMDiff โˆž (uncurry f)) (hg : CMDiff โˆž (uncurry g)) (hk : CMDiff โˆž k) (hg' : โˆ€ y x, x โˆ‰ K โ†’ f y (ฯ† x) = ฯˆ (g y x)) : CMDiff โˆž fun x โ†ฆ update ฯ† ฯˆ (f x) (g x) (k x) := by have hK' : โˆ€ x, k x โˆ‰ ฯ† '' K โ†’ update ฯ† ฯˆ (f x) (g x) (k x) = f x (k x) := fun x hx โ†ฆ diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index f67ea804..02d53c36 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -35,7 +35,7 @@ variable {f : N โ†’ Jยน[๐•œ, E, I, M, V]} -- todo: remove or use to prove `contMDiff_one_jet_eucl_bundle` theorem contMDiffAt_one_jet_eucl_bundle' {xโ‚€ : N} : ContMDiffAt J (I.prod ๐“˜(๐•œ, E โ†’L[๐•œ] V)) โˆž f xโ‚€ โ†” CMDiffAt โˆž (fun x โ†ฆ (f x).1) xโ‚€ โˆง - ContMDiffAt J ๐“˜(๐•œ, E โ†’L[๐•œ] V) โˆž (fun x โ†ฆ show E โ†’L[๐•œ] V from + CMDiffAt โˆž (fun x โ†ฆ show E โ†’L[๐•œ] V from (f x).2 โˆ˜L (trivializationAt E (TangentSpace I : M โ†’ _) (f xโ‚€).1).symmL ๐•œ (f x).1) xโ‚€ := by simp_rw [contMDiffAt_hom_bundle, inCoordinates, Trivial.trivializationAt, Trivial.trivialization_continuousLinearMapAt] @@ -45,7 +45,7 @@ theorem contMDiffAt_one_jet_eucl_bundle' {xโ‚€ : N} : theorem contMDiffAt_one_jet_eucl_bundle {xโ‚€ : N} : ContMDiffAt J (I.prod ๐“˜(๐•œ, E โ†’L[๐•œ] V)) โˆž f xโ‚€ โ†” CMDiffAt โˆž (fun x โ†ฆ (f x).1) xโ‚€ โˆง - ContMDiffAt J ๐“˜(๐•œ, E โ†’L[๐•œ] V) โˆž (fun x โ†ฆ show E โ†’L[๐•œ] V from + CMDiffAt โˆž (fun x โ†ฆ show E โ†’L[๐•œ] V from (f x).2 โˆ˜L (trivializationAt E (TangentSpace I) (f xโ‚€).proj).symmL ๐•œ (f x).proj) xโ‚€ := by rw [contMDiffAt_hom_bundle, and_congr_right_iff] intro hf @@ -62,7 +62,7 @@ theorem contMDiffAt_one_jet_eucl_bundle {xโ‚€ : N} : theorem ContMDiffAt.one_jet_eucl_bundle_mk' {f : N โ†’ M} {ฯ• : N โ†’ E โ†’L[๐•œ] V} {xโ‚€ : N} (hf : CMDiffAt โˆž f xโ‚€) - (hฯ• : ContMDiffAt J ๐“˜(๐•œ, E โ†’L[๐•œ] V) โˆž (fun x โ†ฆ show E โ†’L[๐•œ] V from + (hฯ• : CMDiffAt โˆž (fun x โ†ฆ show E โ†’L[๐•œ] V from ฯ• x โˆ˜L (trivializationAt E (TangentSpace I : M โ†’ _) (f xโ‚€)).symmL ๐•œ (f x)) xโ‚€) : ContMDiffAt J (I.prod ๐“˜(๐•œ, E โ†’L[๐•œ] V)) โˆž (fun x โ†ฆ Bundle.TotalSpace.mk (f x) (ฯ• x) : N โ†’ Jยน[๐•œ, E, I, M, V]) xโ‚€ := @@ -70,7 +70,7 @@ theorem ContMDiffAt.one_jet_eucl_bundle_mk' {f : N โ†’ M} {ฯ• : N โ†’ E โ†’L[ theorem ContMDiffAt.one_jet_eucl_bundle_mk {f : N โ†’ M} {ฯ• : N โ†’ E โ†’L[๐•œ] V} {xโ‚€ : N} (hf : CMDiffAt โˆž f xโ‚€) - (hฯ• : ContMDiffAt J ๐“˜(๐•œ, E โ†’L[๐•œ] V) โˆž (fun x โ†ฆ show E โ†’L[๐•œ] V from + (hฯ• : CMDiffAt โˆž (fun x โ†ฆ show E โ†’L[๐•œ] V from ฯ• x โˆ˜L (trivializationAt E (TangentSpace I) (f xโ‚€)).symmL ๐•œ (f x)) xโ‚€) : ContMDiffAt J (I.prod ๐“˜(๐•œ, E โ†’L[๐•œ] V)) โˆž (fun x โ†ฆ Bundle.TotalSpace.mk (f x) (ฯ• x) : N โ†’ Jยน[๐•œ, E, I, M, V]) xโ‚€ := @@ -218,9 +218,8 @@ def familyJoin {f : N ร— M โ†’ V} (hf : ContMDiff (J.prod I) ๐“˜(โ„, V) โˆž f) ext : 1 <;> simp def familyTwist (s : OneJetEuclSec I M V) (i : N ร— M โ†’ V โ†’L[โ„] V') - (i_smooth : โˆ€ xโ‚€ : N ร— M, ContMDiffAt (J.prod I) ๐“˜(โ„, V โ†’L[โ„] V') โˆž i xโ‚€) : - FamilyOneJetEuclSec I M V' J N - where + (i_smooth : โˆ€ xโ‚€ : N ร— M, CMDiffAt โˆž i xโ‚€) : + FamilyOneJetEuclSec I M V' J N where toFun p := โŸจp.2, (i p).comp (s p.2).2โŸฉ is_sec' p := rfl smooth' := by diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean b/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean index 9f35ccee..ad44a3ae 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean @@ -31,23 +31,19 @@ variable {๐•œ : Type*} [NontriviallyNormedField ๐•œ] {e : OpenPartialHomeomorph M H} {f : M โ†’ M'} {m n : WithTop โ„•โˆž} {s : Set M} {x x' : M} theorem contMDiff_prod {f : M โ†’ M' ร— N'} : - ContMDiff I (I'.prod J') n f โ†” - (CMDiff n fun x โ†ฆ (f x).1) โˆง CMDiff n fun x โ†ฆ (f x).2 := + CMDiff n f โ†” (CMDiff n fun x โ†ฆ (f x).1) โˆง CMDiff n fun x โ†ฆ (f x).2 := โŸจfun h โ†ฆ โŸจh.fst, h.sndโŸฉ, fun h โ†ฆ h.1.prodMk h.2โŸฉ theorem contMDiffAt_prod {f : M โ†’ M' ร— N'} {x : M} : - ContMDiffAt I (I'.prod J') n f x โ†” - CMDiffAt n (fun x โ†ฆ (f x).1) x โˆง CMDiffAt n (fun x โ†ฆ (f x).2) x := + CMDiffAt n f x โ†” CMDiffAt n (fun x โ†ฆ (f x).1) x โˆง CMDiffAt n (fun x โ†ฆ (f x).2) x := โŸจfun h โ†ฆ โŸจh.fst, h.sndโŸฉ, fun h โ†ฆ h.1.prodMk h.2โŸฉ theorem smooth_prod {f : M โ†’ M' ร— N'} : - ContMDiff I (I'.prod J') โˆž f โ†” - (CMDiff โˆž fun x โ†ฆ (f x).1) โˆง CMDiff โˆž fun x โ†ฆ (f x).2 := + CMDiff โˆž f โ†” (CMDiff โˆž fun x โ†ฆ (f x).1) โˆง CMDiff โˆž fun x โ†ฆ (f x).2 := contMDiff_prod theorem smoothAt_prod {f : M โ†’ M' ร— N'} {x : M} : - ContMDiffAt I (I'.prod J') โˆž f x โ†” - CMDiffAt โˆž (fun x โ†ฆ (f x).1) x โˆง CMDiffAt โˆž (fun x โ†ฆ (f x).2) x := + CMDiffAt โˆž f x โ†” CMDiffAt โˆž (fun x โ†ฆ (f x).1) x โˆง CMDiffAt โˆž (fun x โ†ฆ (f x).2) x := contMDiffAt_prod end IsManifold From 9a33355fef2af2a7cc22847826c48915a1709abd Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 26 Oct 2025 21:53:29 +0100 Subject: [PATCH 4/4] ExistsOfConvex: remove last use of local notation The new elaborators are similarly short --- SphereEversion/ToMathlib/ExistsOfConvex.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index 810df115..a1468f22 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -110,10 +110,6 @@ variable {Hโ‚ Mโ‚ Hโ‚‚ Mโ‚‚ : Type*} [TopologicalSpace Hโ‚‚] (Iโ‚‚ : ModelWithCorners โ„ Eโ‚‚ Hโ‚‚) [TopologicalSpace Mโ‚‚] [ChartedSpace Hโ‚‚ Mโ‚‚] [IsManifold Iโ‚‚ โˆž Mโ‚‚] -@[inherit_doc] local notation "๐“’" => ContMDiff (Iโ‚.prod Iโ‚‚) ๐“˜(โ„, F) - -@[inherit_doc] local notation "๐“’_on" => ContMDiffOn (Iโ‚.prod Iโ‚‚) ๐“˜(โ„, F) - omit [FiniteDimensional โ„ Eโ‚] [FiniteDimensional โ„ Eโ‚‚] [IsManifold Iโ‚ โˆž Mโ‚] [IsManifold Iโ‚‚ โˆž Mโ‚‚] in theorem reallyConvex_contMDiffAtProd {x : Mโ‚} (n : โ„•โˆž) : @@ -135,8 +131,8 @@ omit [FiniteDimensional โ„ Eโ‚‚] [IsManifold Iโ‚‚ โˆž Mโ‚‚] in theorem exists_contMDiff_of_convexโ‚‚ {P : Mโ‚ โ†’ (Mโ‚‚ โ†’ F) โ†’ Prop} [SigmaCompactSpace Mโ‚] [T2Space Mโ‚] (hP : โˆ€ x, Convex โ„ {f | P x f}) {n : โ„•โˆž} (hP' : โˆ€ x : Mโ‚, โˆƒ U โˆˆ ๐“ x, โˆƒ f : Mโ‚ โ†’ Mโ‚‚ โ†’ F, - ๐“’_on n (uncurry f) (U ร—หข (univ : Set Mโ‚‚)) โˆง โˆ€ y โˆˆ U, P y (f y)) : - โˆƒ f : Mโ‚ โ†’ Mโ‚‚ โ†’ F, ๐“’ n (uncurry f) โˆง โˆ€ x, P x (f x) := by + CMDiff[U ร—หข (univ : Set Mโ‚‚)] n (uncurry f) โˆง โˆ€ y โˆˆ U, P y (f y)) : + โˆƒ f : Mโ‚ โ†’ Mโ‚‚ โ†’ F, CMDiff n (uncurry f) โˆง โˆ€ x, P x (f x) := by let PP : (ฮฃ x : Mโ‚, Germ (๐“ x) (Mโ‚‚ โ†’ F)) โ†’ Prop := fun p โ†ฆ p.2.ContMDiffAtProd Iโ‚ Iโ‚‚ n โˆง P p.1 p.2.value have hPP : โˆ€ x : Mโ‚, ReallyConvex (smoothGerm Iโ‚ x) {ฯ† | PP โŸจx, ฯ†โŸฉ} := fun x โ†ฆ by