WIP: bump mathlib. One file moved, one tiny PR landed.

Four proofs broke in which I cannot easily fix.

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 :=

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}

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) :

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)

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

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
 

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

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)

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,

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,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1