From 6a8877253d00795becf6c63f55fe644ef446ee72 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sun, 5 May 2024 12:28:20 +0200 Subject: [PATCH] WIP: bump mathlib. One file moved, one tiny PR landed. Four proofs broke in which I cannot easily fix. --- SphereEversion/Global/Immersion.lean | 2 +- SphereEversion/Global/ParametricityForFree.lean | 8 ++++++-- SphereEversion/Global/SmoothEmbedding.lean | 4 ++-- SphereEversion/Local/AmpleSet.lean | 8 -------- SphereEversion/Loops/Reparametrization.lean | 1 + SphereEversion/ToMathlib/Analysis/Calculus.lean | 2 +- .../Analysis/InnerProductSpace/Rotation.lean | 3 +-- .../Geometry/Manifold/Algebra/SmoothGerm.lean | 5 +++-- SphereEversion/ToMathlib/Topology/Path.lean | 2 +- lake-manifest.json | 14 +++++++------- lean-toolchain | 2 +- 11 files changed, 24 insertions(+), 27 deletions(-) diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 19509b04..46defdf3 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -176,7 +176,7 @@ def formalEversionAux : FamilyOneJetSec (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ, refine (ω.contDiff_rot ?_).contMDiffAt exact ne_zero_of_mem_unit_sphere p.2 refine this.comp p (Smooth.smoothAt ?_) - exact smooth_fst.prod_mk (contMDiff_coe_sphere.comp smooth_snd)) + sorry /- TODO-BUMP(4.8-rc1) was `exact smooth_fst.prod_mk (contMDiff_coe_sphere.comp smooth_snd))` -/) /-- A formal eversion of a two-sphere into its ambient Euclidean space. -/ def formalEversionAux2 : HtpyFormalSol 𝓡_imm := diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index 8e85c77d..e3a4d571 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -96,9 +96,13 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'} (show E' from σ.2 (p.v - (id (0, (q.v : E)) : TangentSpace (IP.prod I) σ.proj.1))) (show Set E' from R.slice (bundleSnd σ) q) dsimp only at this - erw [← this, mem_preimage, mem_slice, R.mem_relativize] + save + erw [← this] + rw [mem_preimage] + sorry /- TODO-BUMP(4.8-rc1): remaining proof was + erw [mem_slice, R.mem_relativize] dsimp only [oneJetBundle_mk_fst, oneJetBundle_mk_snd] - congr! + congr! -/ theorem relativize_slice_eq_univ {σ : OneJetBundle (IP.prod I) (P × M) I' M'} {p : DualPair <| TangentSpace (IP.prod I) σ.1.1} diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index d83777f5..1d89368e 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -92,7 +92,7 @@ theorem coe_comp_invFun_eventuallyEq (x : M) : f ∘ f.invFun =ᶠ[𝓝 (f x)] i (by intro v erw [← ContinuousLinearMap.comp_apply, ← mfderiv_comp x h₁ h₂, f.invFun_comp_coe, mfderiv_id, - ContinuousLinearMap.coe_id', id.def]) + ContinuousLinearMap.coe_id', id]) (by intro v have hx : x = f.invFun (f x) := by rw [f.left_inv] @@ -101,7 +101,7 @@ theorem coe_comp_invFun_eventuallyEq (x : M) : f ∘ f.invFun =ᶠ[𝓝 (f x)] i erw [hx, hx', ← ContinuousLinearMap.comp_apply, ← mfderiv_comp (f x) h₂ h₁, ((hasMFDerivAt_id I' (f x)).congr_of_eventuallyEq (f.coe_comp_invFun_eventuallyEq x)).mfderiv, - ContinuousLinearMap.coe_id', id.def]) + ContinuousLinearMap.coe_id', id]) @[simp] theorem fderiv_coe (x : M) : diff --git a/SphereEversion/Local/AmpleSet.lean b/SphereEversion/Local/AmpleSet.lean index 511d7d29..59ee4c36 100644 --- a/SphereEversion/Local/AmpleSet.lean +++ b/SphereEversion/Local/AmpleSet.lean @@ -51,11 +51,3 @@ theorem AmpleSet.of_one_lt_codim {E : Submodule ℝ F} (hcodim : 1 < Module.rank · exact subset_convexHull ℝ (Eᶜ : Set F) h end Lemma213 - -open scoped Pointwise --- PRed in #12046 -/-- Affine translations of ample sets are ample. -/ -theorem AmpleSet.vadd {E : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] - {s : Set E} (h : AmpleSet s) {y : E} : - AmpleSet (y +ᵥ s) := - h.image (ContinuousAffineEquiv.constVAdd ℝ E y) diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index da1fabdf..ece96973 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -466,6 +466,7 @@ theorem reparametrize_smooth : 𝒞 ∞ <| uncurry fun (x : E) (t : ℝ) ↦ γ. apply contDiff_parametric_symm_of_deriv_pos · exact contDiff_parametric_primitive_of_contDiff'' γ.centeringDensity_smooth 0 · exact fun x ↦ deriv_integral_centeringDensity_pos γ x + sorry /- TODO-BUMP(4.8-rc1); original proof was done now -/ @[simp] theorem reparametrize_average : ((γ x).reparam <| (γ.reparametrize x).equivariantMap).average = g x := by diff --git a/SphereEversion/ToMathlib/Analysis/Calculus.lean b/SphereEversion/ToMathlib/Analysis/Calculus.lean index b4da44a5..b20363cf 100644 --- a/SphereEversion/ToMathlib/Analysis/Calculus.lean +++ b/SphereEversion/ToMathlib/Analysis/Calculus.lean @@ -193,7 +193,7 @@ theorem ContDiff.contDiff_top_partial_snd {φ : E → F → G} (hF : ContDiff end Calculus -section RealCalculus +section RealCalculus -- PRed in #12673 open ContinuousLinearMap diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean index ea5402eb..15acf0d2 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean @@ -6,7 +6,6 @@ Authors: Heather Macbeth ! This file was ported from Lean 3 source module to_mathlib.analysis.inner_product_space.rotation -/ import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv - import SphereEversion.ToMathlib.Analysis.ContDiff import SphereEversion.ToMathlib.LinearAlgebra.Basic import SphereEversion.ToMathlib.Analysis.InnerProductSpace.CrossProduct @@ -148,7 +147,7 @@ theorem injOn_rot_of_ne (t : ℝ) {x : E} (hx : x ≠ 0) : Set.InjOn (ω.rot (t, simp_rw [← pow_two, norm_smul, mul_pow] at hy change _ + _ * ‖x×₃(⟨y, hy'⟩ : (span ℝ {x})ᗮ)‖ ^ 2 = ‖(0 : E)‖ ^ 2 at hy rw [norm_crossProduct] at hy - simp only [norm_eq_abs, Even.pow_abs, coe_mk, norm_zero, zero_pow, Ne.def, + simp only [norm_eq_abs, Even.pow_abs, coe_mk, norm_zero, zero_pow, Ne, Nat.one_ne_zero, not_false_iff] at hy change _ + _ * (_ * ‖y‖) ^ 2 = 0 at hy rw [mul_pow, ← mul_assoc, ← add_mul, mul_eq_zero, or_iff_not_imp_left] at hy diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean index 65bce9ba..94ea53e1 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Patrick Massot -/ +import Mathlib.Algebra.Ring.Subring.Order import Mathlib.Geometry.Manifold.Algebra.SmoothFunctions import Mathlib.Geometry.Manifold.MFDeriv.Basic import Mathlib.Topology.Germ -import Mathlib.RingTheory.Subring.Order /-! ## Germs of smooth functions @@ -289,7 +289,8 @@ theorem ContMDiffAtProd.sum {x : M₁} {ι} {s : Finset ι} {n : ℕ∞} (∑ i in s, f i).ContMDiffAtProd I₁ I₂ n := by classical induction' s using Finset.induction_on with φ s hφs hs - · rw [Finset.sum_empty]; intro y; exact contMDiffAt_const + · rw [Finset.sum_empty]; intro y + sorry /- TODO-BUMP(4.8-rc1): proof was `exact contMDiffAt_const` -/ simp only [Finset.mem_insert, forall_eq_or_imp] at h rw [Finset.sum_insert hφs] exact h.1.add (hs h.2) diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean index e2418502..626303c5 100644 --- a/SphereEversion/ToMathlib/Topology/Path.lean +++ b/SphereEversion/ToMathlib/Topology/Path.lean @@ -29,7 +29,7 @@ def strans (γ γ' : Path x x) (t₀ : I) : Path x x where refine Continuous.if_le ?_ ?_ continuous_id continuous_const ?_ · continuity · continuity - · simp only [extend_div_self, Icc.mk_zero, zero_le_one, id.def, zero_div, forall_eq, + · simp only [extend_div_self, Icc.mk_zero, zero_le_one, id, zero_div, forall_eq, extend_extends, Path.source, left_mem_Icc, sub_self] source' := by simp only [unitInterval.nonneg', Icc.coe_zero, Icc.mk_zero, zero_le_one, if_true, zero_div, diff --git a/lake-manifest.json b/lake-manifest.json index bd1a1eb3..9d81ce2a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", + "rev": "3025cb124492b423070f20cf0a70636f757d117f", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", + "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,16 +31,16 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", + "rev": "fe1eff53bd0838c657aa6126fe4dd75ad9939d9a", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", + "inputRev": "v0.0.35", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", + "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", + "rev": "188eb34fcf1125e89d651ad462d02598219718ca", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "48970a4b9d58c67ee28352df33fc0dfffe98d99c", + "rev": "c1f040b7f1014c9eda2f5b9accb7dca9ed7ae097", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 9ad30404..d8a6d7ef 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.8.0-rc1