Bump to 4.10.0-rc2 (current mathlib).

- Using LocalisationData needed much more elaboration, unclear why
- Filter/Germ was split in two, as was Calculus/AffineMap

- Fix deprecation warnings; remove some easy use of refine'.
Three instances will remain for now.

- Continuity of parametric integrals has landed in mathlib (namespaced) \o/

SphereEversion.lean

@@ -28,7 +28,7 @@ import SphereEversion.Main
 import SphereEversion.Notations
 import SphereEversion.ToMathlib.Algebra.Periodic
 import SphereEversion.ToMathlib.Analysis.Calculus
-import SphereEversion.ToMathlib.Analysis.Calculus.AffineMap
+import SphereEversion.ToMathlib.Analysis.Calculus.AddTorsor.AffineMap
 import SphereEversion.ToMathlib.Analysis.ContDiff
 import SphereEversion.ToMathlib.Analysis.Convex.Basic
 import SphereEversion.ToMathlib.Analysis.CutOff

SphereEversion/Global/LocalisationData.lean

@@ -33,7 +33,9 @@ structure LocalisationData (f : M → M') where
 
 namespace LocalisationData
 
-variable {f : M → M'} {I I'} (ld : LocalisationData I I' f)
+-- Adaptation note(version 4.10-rc1): previously, specifying 𝕜, E, E', H and H' was not needed
+variable {f : M → M'} {I I'}
+  (ld : LocalisationData (𝕜 := 𝕜) (E := E) (E' := E') (H := H) (H' := H')  I I' f)
 
 abbrev ψj : IndexType ld.N → OpenSmoothEmbedding 𝓘(𝕜, E') E' I' M' :=
   ld.ψ ∘ ld.j

SphereEversion/Global/OneJetSec.lean

@@ -5,7 +5,7 @@ Authors: Patrick Massot, Floris van Doorn
 
 ! This file was ported from Lean 3 source module global.one_jet_sec
 -/
-import Mathlib.Order.Filter.Germ
+import Mathlib.Order.Filter.Germ.Basic
 import SphereEversion.ToMathlib.Topology.Algebra.Module
 import SphereEversion.Global.OneJetBundle
 

SphereEversion/Local/Corrugation.lean

@@ -33,7 +33,6 @@ The main definition is `corrugation`. The main results are:
 noncomputable section
 
 open Set Function Filter MeasureTheory ContinuousLinearMap
-
 open scoped Topology unitInterval
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
@@ -88,6 +87,7 @@ theorem corrugation.support : support (𝒯 N γ) ⊆ Loop.support γ := fun x x
 theorem corrugation_eq_zero (x) (H : x ∉ Loop.support γ) : corrugation π N γ x = 0 :=
   nmem_support.mp fun hx ↦ H (corrugation.support π N γ hx)
 
+open intervalIntegral in
 theorem corrugation.c0_small_on [FirstCountableTopology E] [LocallyCompactSpace E]
     {γ : ℝ → E → Loop F} {K : Set E} (hK : IsCompact K) (h_le : ∀ x, ∀ t ≤ 0, γ t x = γ 0 x)
     (h_ge : ∀ x, ∀ t ≥ 1, γ t x = γ 1 x) (hγ_cont : Continuous ↿γ) {ε : ℝ} (ε_pos : 0 < ε) :

SphereEversion/Local/OneJet.lean

@@ -217,7 +217,7 @@ theorem smoothStep.mem (t : ℝ) : smoothStep t ∈ I :=
   ⟨smoothTransition.nonneg _, smoothTransition.le_one _⟩
 
 theorem smoothStep.abs_le (t : ℝ) : |smoothStep t| ≤ 1 :=
-  abs_le.mpr ⟨by linarith [(smoothStep.mem t).1], smoothTransition.le_one _⟩
+  _root_.abs_le.mpr ⟨by linarith [(smoothStep.mem t).1], by apply smoothTransition.le_one _⟩
 
 theorem smoothStep.of_lt {t : ℝ} (h : t < 1 / 4) : smoothStep t = 0 := by
   apply smoothTransition.zero_of_nonpos

SphereEversion/Loops/Basic.lean

@@ -6,10 +6,9 @@ import SphereEversion.ToMathlib.MeasureTheory.ParametricIntervalIntegral
 # Basic definitions and properties of loops
 -/
 
-
 open Set Function FiniteDimensional Int TopologicalSpace
 
-open scoped BigOperators Topology unitInterval
+open scoped Topology unitInterval
 
 noncomputable section
 
@@ -334,7 +333,7 @@ theorem isConst_of_not_mem_support {γ : X → Loop F} {x : X} (hx : x ∉ suppo
 theorem continuous_average {E : Type*} [TopologicalSpace E] [FirstCountableTopology E]
     [LocallyCompactSpace E] {γ : E → Loop F} (hγ_cont : Continuous ↿γ) :
     Continuous fun x ↦ (γ x).average :=
-  continuous_parametric_intervalIntegral_of_continuous' hγ_cont _ _
+  intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' (by apply hγ_cont) _ _
 
 /-- The normalization of a loop `γ` is the loop `γ - γ.average`. -/
 def normalize (γ : Loop F) : Loop F where

SphereEversion/Loops/Exists.lean

@@ -70,7 +70,7 @@ theorem exist_loops_aux1 (hK : IsCompact K) (hΩ_op : IsOpen Ω) (hb : 𝒞 ∞
     have : ‖ε • γ₀ t s‖ < ε₀ := (h2ε t s).trans (h0ε₁ ▸ half_lt_self hε₀)
     exact h1 x hx t s (by simpa [γ₁, ← h0ε₁])
   · intro x hx
-    rw [← h0ε₁, add_halves']
+    rw [← h0ε₁, add_halves]
     exact (ball_subset_thickening (mem_image_of_mem _ hx.2) _).trans hεΩ
   · rintro x ⟨-, -⟩ t s
     simp [γ₁, h2ε]
@@ -214,7 +214,7 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op :
   · rintro x - t - s -; rw [← not_mem_compl_iff]
     by_cases hΩ : Ωᶜ.Nonempty; swap
     · rw [not_nonempty_iff_eq_empty] at hΩ; rw [hΩ]; apply not_mem_empty
-    refine' not_mem_of_dist_lt_infDist ?_
+    refine not_mem_of_dist_lt_infDist (x := ?_) ?_
     · exact (x, γ₃ x (smoothTransition t) (fract s))
     · rw [dist_comm, dist_prod_same_left]
       refine (hγ₅₄ (x, _, fract s)).trans_le ((min_le_right _ _).trans <| csInf_le ?_ ?_)

SphereEversion/Loops/Reparametrization.lean

@@ -81,7 +81,7 @@ theorem Loop.tendsto_mollify_apply (γ : E → Loop F) (h : Continuous ↿γ) (x
       exact this.comp ((tendsto_fst.comp tendsto_fst).prod_mk tendsto_snd)
   · rw [← zero_smul ℝ (_ : F)]
     have : Continuous fun z ↦ intervalIntegral (γ z) 0 1 volume :=
-      continuous_parametric_intervalIntegral_of_continuous (by apply h) continuous_const
+      intervalIntegral.continuous_parametric_intervalIntegral_of_continuous (by apply h) continuous_const
     exact (tendsto_one_div_add_atTop_nhds_zero_nat.comp tendsto_snd).smul
       ((this.tendsto x).comp tendsto_fst)
 

SphereEversion/ToMathlib/Algebra/Periodic.lean

@@ -106,7 +106,7 @@ theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁ := QuotientAddGroup.isOpen
 theorem quotientMap_id_proj𝕊₁ {X : Type*} [TopologicalSpace X] :
     QuotientMap fun p : X × ℝ ↦ (p.1, proj𝕊₁ p.2) :=
   (IsOpenMap.id.prod isOpenMap_proj𝕊₁).to_quotientMap (continuous_id.prod_map continuous_proj𝕊₁)
-    (surjective_id.Prod_map Quotient.exists_rep)
+    (surjective_id.prodMap Quotient.exists_rep)
 
 /-- A one-periodic function on `ℝ` descends to a function on the circle `ℝ ⧸ ℤ`. -/
 def OnePeriodic.lift {f : ℝ → α} (h : OnePeriodic f) : 𝕊₁ → α :=

SphereEversion/ToMathlib/Analysis/Calculus/AffineMap.lean → SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean

@@ -1,4 +1,4 @@
-import Mathlib.Analysis.Calculus.AffineMap
+import Mathlib.Analysis.Calculus.AddTorsor.AffineMap
 
 /-!
 

SphereEversion/ToMathlib/Analysis/ContDiff.lean

@@ -202,7 +202,7 @@ theorem contDiff_parametric_symm_of_deriv_pos {f : E → ℝ → ℝ} (hf : Cont
   have hmono := fun x ↦ strictMono_of_deriv_pos (hderiv x)
   let F x := (StrictMono.orderIsoOfSurjective (f x) (hmono x) <| hsurj x).toEquiv
   change ContDiff ℝ ⊤ fun p : E × ℝ ↦ (F p.1).symm p.snd
-  refine' contDiff_parametric_symm hf ?_
+  refine contDiff_parametric_symm hf (f' := ?_) ?_
   · exact fun x t ↦
       ContinuousLinearEquiv.unitsEquivAut ℝ (Units.mk0 (deriv (f x) t) <| ne_of_gt (hderiv x t))
   · intro x t

SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm.lean

@@ -11,12 +11,12 @@ variable {𝕜 E F G Fₗ Gₗ X : Type*} [NontriviallyNormedField 𝕜] [Normed
   [NormedSpace 𝕜 E] [NormedSpace 𝕜 Fₗ] [NormedSpace 𝕜 Gₗ] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G]
   [TopologicalSpace X]
 
-theorem ContinuousLinearMap.le_op_norm_of_le' {𝕜 : Type*} {𝕜₂ : Type*} {E : Type*} {F : Type*}
+theorem ContinuousLinearMap.le_opNorm_of_le' {𝕜 : Type*} {𝕜₂ : Type*} {E : Type*} {F : Type*}
     [NormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜]
     [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂}
     [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) {x : E} (hx : x ≠ 0) {C : ℝ} (h : C * ‖x‖ ≤ ‖f x‖) :
     C ≤ ‖f‖ := by
-  apply le_of_mul_le_mul_right (h.trans (f.le_op_norm x))
+  apply le_of_mul_le_mul_right (h.trans (f.le_opNorm x))
   rwa [norm_pos_iff']
 
 @[simp]
@@ -78,7 +78,7 @@ theorem isBoundedLinearMap_coprod (𝕜 : Type*) [NontriviallyNormedField 𝕜]
       rintro ⟨e, f⟩
       calc
         ‖φ e + ψ f‖ ≤ ‖φ e‖ + ‖ψ f‖ := norm_add_le _ _
-        _ ≤ ‖φ‖ * ‖e‖ + ‖ψ‖ * ‖f‖ := (add_le_add (φ.le_op_norm e) (ψ.le_op_norm f))
+        _ ≤ ‖φ‖ * ‖e‖ + ‖ψ‖ * ‖f‖ := (add_le_add (φ.le_opNorm e) (ψ.le_opNorm f))
         _ ≤ 2 * max ‖φ‖ ‖ψ‖ * max ‖e‖ ‖f‖ := by
           rw [two_mul, add_mul]
           gcongr <;> first | apply le_max_left | apply le_max_right }

SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean

@@ -6,53 +6,6 @@ import SphereEversion.ToMathlib.Analysis.Calculus
 open TopologicalSpace MeasureTheory Filter FirstCountableTopology Metric Set Function
 open scoped Topology
 
-section -- PRed in #11185
-
-variable {μ : Measure ℝ} [IsLocallyFiniteMeasure μ] [NoAtoms μ]
-  {X : Type*} [TopologicalSpace X] [FirstCountableTopology X]
-  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
-
-theorem continuous_parametric_primitive_of_continuous [LocallyCompactSpace X] {F : X → ℝ → E}
-    {a₀ : ℝ} (hF : Continuous fun p : X × ℝ ↦ F p.1 p.2) :
-    Continuous fun p : X × ℝ ↦ ∫ t in a₀..p.2, F p.1 t ∂μ := by
-  rw [continuous_iff_continuousAt]
-  rintro ⟨x₀, b₀⟩
-  rcases exists_compact_mem_nhds x₀ with ⟨U, U_cpct, U_nhds⟩
-  cases' exists_lt (min a₀ b₀) with a a_lt
-  cases' exists_gt (max a₀ b₀) with b lt_b
-  rw [lt_min_iff] at a_lt
-  rw [max_lt_iff] at lt_b
-  have a₀_in : a₀ ∈ Ioo a b := ⟨a_lt.1, lt_b.1⟩
-  have b₀_in : b₀ ∈ Ioo a b := ⟨a_lt.2, lt_b.2⟩
-  obtain ⟨M, hM⟩ :=
-    (U_cpct.prod (isCompact_Icc (a := a) (b := b))).bddAbove_image hF.norm.continuousOn
-  refine intervalIntegral.continuousAt_parametric_primitive_of_dominated
-    (fun _ ↦ M) a b ?_ ?_ ?_ ?_ a₀_in b₀_in (measure_singleton b₀)
-  · exact fun x ↦ (hF.comp (Continuous.Prod.mk x)).aestronglyMeasurable
-  · refine Eventually.mono U_nhds fun x (x_in : x ∈ U) ↦ ?_
-    simp_rw [ae_restrict_iff' measurableSet_uIoc]
-    refine eventually_of_forall fun t t_in ↦ ?_
-    refine hM (mem_image_of_mem _ <| mk_mem_prod x_in ?_)
-    rw [uIoc_of_le (a_lt.1.trans lt_b.1).le] at t_in
-    exact mem_Icc_of_Ioc t_in
-  · apply intervalIntegrable_const
-  · apply ae_of_all
-    intro a
-    apply (hF.comp₂ continuous_id continuous_const).continuousAt
-
-theorem continuous_parametric_intervalIntegral_of_continuous [LocallyCompactSpace X] {a₀ : ℝ}
-    {F : X → ℝ → E} (hF : Continuous fun p : X × ℝ ↦ F p.1 p.2) {s : X → ℝ} (hs : Continuous s) :
-    Continuous fun x ↦ ∫ t in a₀..s x, F x t ∂μ :=
-  show Continuous ((fun p : X × ℝ ↦ ∫ t in a₀..p.2, F p.1 t ∂μ) ∘ fun x ↦ (x, s x)) from
-    (continuous_parametric_primitive_of_continuous hF).comp₂ continuous_id hs
-
-theorem continuous_parametric_intervalIntegral_of_continuous' [LocallyCompactSpace X]
-    {F : X → ℝ → E} (hF : Continuous fun p : X × ℝ ↦ F p.1 p.2) (a₀ b₀ : ℝ) :
-    Continuous fun x ↦ ∫ t in a₀..b₀, F x t ∂μ :=
-  continuous_parametric_intervalIntegral_of_continuous hF continuous_const
-
-end
-
 section
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
@@ -63,7 +16,6 @@ We could weaken `FiniteDimensional ℝ H` with `SecondCountable (H →L[ℝ] E)`
 but that is less convenient to work with.
 -/
 
-
 open Real ContinuousLinearMap Asymptotics
 
 /-- This statement is a new version using the continuity note in mathlib.
@@ -270,7 +222,7 @@ theorem contDiff_parametric_primitive_of_contDiff' {F : H → ℝ → E} {n : 
     {s : H → ℝ} (hs : ContDiff ℝ n s) (a : ℝ) : ContDiff ℝ n fun x : H ↦ ∫ t in a..s x, F x t := by
   induction' n with n ih generalizing F
   · rw [Nat.cast_zero, contDiff_zero] at *
-    exact continuous_parametric_intervalIntegral_of_continuous hF hs
+    exact intervalIntegral.continuous_parametric_intervalIntegral_of_continuous hF hs
   · have hF₁ : ContDiff ℝ 1 ↿F := hF.one_of_succ
     have hs₁ : ContDiff ℝ 1 s := hs.one_of_succ
     have h :

SphereEversion/ToMathlib/SmoothBarycentric.lean

@@ -1,12 +1,13 @@
+import Mathlib.Analysis.Calculus.AddTorsor.Coord
 import Mathlib.Analysis.Matrix
-import Mathlib.LinearAlgebra.AffineSpace.Matrix
 import Mathlib.Analysis.NormedSpace.AddTorsorBases
+import Mathlib.LinearAlgebra.AffineSpace.Matrix
 
 noncomputable section
 
 open Set Function
 
-open scoped Affine Matrix BigOperators
+open scoped Affine Matrix
 
 section BarycentricDet
 

SphereEversion/ToMathlib/Topology/Separation.lean

@@ -16,4 +16,4 @@ theorem t2Space_iff_of_continuous_surjective_open {α β : Type*} [TopologicalSp
   · exact H.preimage (hcont.prod_map hcont)
   · simp_rw [← isOpen_compl_iff] at H ⊢
     convert hop.prod hop _ H
-    exact ((hsurj.Prod_map hsurj).image_preimage _).symm
+    exact ((hsurj.prodMap hsurj).image_preimage _).symm

lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
+   "scope": "leanprover-community",
+   "rev": "ac82ca1064a77eb76d37ae2ab2d1cdeb942d57fe",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,6 +14,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc",
+   "scope": "leanprover-community",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.38",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71",
+   "scope": "leanprover-community",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,15 +64,17 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab",
+   "scope": "",
+   "rev": "b9f14eb6cb84c8af185bb92bd5482208f2070f5c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.9.0",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5",
    "name": "checkdecls",
    "manifestFile": "lake-manifest.json",

lakefile.lean

@@ -8,7 +8,7 @@ package «SphereEversion» where
     ⟨`relaxedAutoImplicit, false⟩]
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.9.0"
+  "https://github.com/leanprover-community/mathlib4.git"
 
 @[default_target]
 lean_lib «SphereEversion» where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.10.0-rc2