chore: bump to Lean 4.13.0

- two imports got moved/split; moved on ToMathlib file accordingly
- the usual renaming/deprecations of lemmas
- three small lemmas got upstreamed to mathlib, by someone else
- FiniteDimensional.finrank got renamed to Module.finrank
(by far the biggest source of breakage)
- the model with corners is now implicit in some diff. geometry lemmas
- various smaller things

SphereEversion.lean

@@ -61,5 +61,5 @@ import SphereEversion.ToMathlib.Topology.HausdorffDistance
 import SphereEversion.ToMathlib.Topology.Misc
 import SphereEversion.ToMathlib.Topology.Paracompact
 import SphereEversion.ToMathlib.Topology.Path
-import SphereEversion.ToMathlib.Topology.Separation
+import SphereEversion.ToMathlib.Topology.Separation.Basic
 import SphereEversion.ToMathlib.Unused.Fin

SphereEversion/Global/Gromov.lean

@@ -105,9 +105,9 @@ theorem RelMfld.Ample.satisfiesHPrinciple' (hRample : R.Ample) (hRopen : IsOpen
     have K₁φ : K₁ ⊆ range φ := SurjOn.subset_range hK₁
     have K₀φ : K₀ ⊆ range φ := K₀K₁.trans interior_subset |>.trans K₁φ
     replace K₀_cpct : IsCompact (φ ⁻¹' K₀) :=
-      φ.openEmbedding.toInducing.isCompact_preimage' K₀_cpct K₀φ
+      φ.openEmbedding.toIsInducing.isCompact_preimage' K₀_cpct K₀φ
     replace K₁_cpct : IsCompact (φ ⁻¹' K₁) :=
-      φ.openEmbedding.toInducing.isCompact_preimage' K₁_cpct K₁φ
+      φ.openEmbedding.toIsInducing.isCompact_preimage' K₁_cpct K₁φ
     have K₀K₁' : φ ⁻¹' K₀ ⊆ interior (φ ⁻¹' K₁) := by
       rw [← φ.isOpenMap.preimage_interior_eq_interior_preimage φ.continuous]
       gcongr

SphereEversion/Global/Immersion.lean

@@ -9,7 +9,7 @@ import SphereEversion.Global.TwistOneJetSec
 -- set_option trace.filter_inst_type true
 noncomputable section
 
-open Metric FiniteDimensional Set Function LinearMap Filter ContinuousLinearMap
+open Metric Module Set Function LinearMap Filter ContinuousLinearMap
 
 open scoped Manifold Topology
 

SphereEversion/Global/OneJetSec.lean

@@ -267,7 +267,7 @@ theorem isHolonomicAt_uncurry (S : FamilyOneJetSec I M I' M' IP P) {p : P × M}
     S.uncurry.IsHolonomicAt p ↔ (S p.1).IsHolonomicAt p.2 := by
   simp_rw [OneJetSec.IsHolonomicAt, OneJetSec.snd_eq, S.uncurry_ϕ]
   rw [show S.uncurry.bs = fun x ↦ S.uncurry.bs x from rfl, funext S.uncurry_bs]
-  simp_rw [mfderiv_prod_eq_add _ _ _ (S.smooth_bs.mdifferentiable _), mfderiv_snd, add_right_inj]
+  simp_rw [mfderiv_prod_eq_add (S.smooth_bs.mdifferentiable _), mfderiv_snd, add_right_inj]
   erw [mfderiv_comp p S.smooth_coe_bs.mdifferentiableAt smooth_snd.mdifferentiableAt, mfderiv_snd]
   exact (show Surjective (ContinuousLinearMap.snd ℝ EP E) from
     Prod.snd_surjective).clm_comp_injective.eq_iff

SphereEversion/Global/ParametricityForFree.lean

@@ -207,7 +207,7 @@ theorem FamilyOneJetSec.curry_ϕ' (S : FamilyOneJetSec (IP.prod I) (P × M) I' M
     (x : M) : (S.curry p).ϕ x = (S p.1).ϕ (p.2, x) ∘L ContinuousLinearMap.inr ℝ EP E := by
   rw [S.curry_ϕ]
   congr 1
-  refine ((mdifferentiableAt_const I IP).mfderiv_prod smooth_id.mdifferentiableAt).trans ?_
+  refine (mdifferentiableAt_const.mfderiv_prod smooth_id.mdifferentiableAt).trans ?_
   rw [mfderiv_id, mfderiv_const]
   rfl
 
@@ -220,7 +220,7 @@ theorem FamilyOneJetSec.isHolonomicAt_curry (S : FamilyOneJetSec (IP.prod I) (P
   simp_rw [OneJetSec.IsHolonomicAt, (S.curry _).snd_eq, S.curry_ϕ] at hS ⊢
   rw [show (S.curry (t, s)).bs = fun x ↦ (S.curry (t, s)).bs x from rfl, funext (S.curry_bs _)]
   refine (mfderiv_comp x (S t).smooth_bs.mdifferentiableAt
-    ((mdifferentiableAt_const I IP).prod_mk smooth_id.mdifferentiableAt)).trans
+    (mdifferentiableAt_const.prod_mk smooth_id.mdifferentiableAt)).trans
     ?_
   rw [id, hS]
   rfl

SphereEversion/Global/SmoothEmbedding.lean

@@ -1,5 +1,7 @@
+import Mathlib.Analysis.Normed.Order.Lattice
+import Mathlib.Geometry.Manifold.ContMDiff.Atlas
+import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
 import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
-import Mathlib.Topology.Algebra.Order.Compact
 import SphereEversion.Indexing
 import SphereEversion.Notations
 import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc
@@ -100,19 +102,22 @@ def fderiv (x : M) : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x) :=
       have hx' : f (f.invFun (f x)) = f x := by rw [f.left_inv]
       rw [hx] at h₂
       erw [hx, hx', ← ContinuousLinearMap.comp_apply, ← mfderiv_comp (f x) h₂ h₁,
-        ((hasMFDerivAt_id I' (f x)).congr_of_eventuallyEq
+        ((hasMFDerivAt_id (f x)).congr_of_eventuallyEq
             (f.coe_comp_invFun_eventuallyEq x)).mfderiv,
         ContinuousLinearMap.coe_id', id])
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 @[simp]
 theorem fderiv_coe (x : M) :
     (f.fderiv x : TangentSpace I x →L[𝕜] TangentSpace I' (f x)) = mfderiv I I' f x := by ext; rfl
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 @[simp]
 theorem fderiv_symm_coe (x : M) :
     ((f.fderiv x).symm : TangentSpace I' (f x) →L[𝕜] TangentSpace I x) =
       mfderiv I' I f.invFun (f x) := by ext; rfl
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 theorem fderiv_symm_coe' {x : M'} (hx : x ∈ range f) :
     ((f.fderiv (f.invFun x)).symm :
         TangentSpace I' (f (f.invFun x)) →L[𝕜] TangentSpace I (f.invFun x)) =
@@ -123,11 +128,11 @@ end
 
 open Filter
 
-theorem openEmbedding : OpenEmbedding f :=
-  openEmbedding_of_continuous_injective_open f.continuous f.injective f.isOpenMap
+theorem openEmbedding : IsOpenEmbedding f :=
+  isOpenEmbedding_of_continuous_injective_open f.continuous f.injective f.isOpenMap
 
-theorem inducing : Inducing f :=
-  f.openEmbedding.toInducing
+theorem inducing : IsInducing f :=
+  f.openEmbedding.toIsInducing
 
 theorem forall_near' {P : M → Prop} {A : Set M'} (h : ∀ᶠ m near f ⁻¹' A, P m) :
     ∀ᶠ m' near A ∩ range f, ∀ m, m' = f m → P m := by
@@ -255,7 +260,7 @@ def openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : PartialHomeomorph F F} (
   isOpen_range :=
     IsOpenMap.isOpen_range fun u hu ↦ by
       have aux : IsOpen (f '' u) := f.isOpen_image_of_subset_source hu (hf₁.symm ▸ subset_univ u)
-      convert isOpen_extChartAt_preimage' IF x aux
+      convert isOpen_extChartAt_preimage' x aux
       rw [image_comp]
       refine
         (extChartAt IF x).symm_image_eq_source_inter_preimage ((image_subset_range f u).trans ?_)
@@ -316,7 +321,7 @@ theorem nice_atlas' {ι : Type*} {s : ι → Set M} (s_op : ∀ j, IsOpen <| s j
     have hV₂ : V ⊆ (extChartAt IF x).target :=
       Subset.trans ((image_subset_range _ _).trans (by simp [h₁])) h₂
     rw [(extChartAt IF x).symm_image_eq_source_inter_preimage hV₂]
-    exact isOpen_extChartAt_preimage' IF x hV₁
+    exact isOpen_extChartAt_preimage' x hV₁
   have hB : ∀ x, (𝓝 x).HasBasis (p x) (B x) := fun x ↦
     ChartedSpace.nhds_hasBasis_balls_of_open_cov IF x s_op cov
   obtain ⟨t, ht₁, ht₂, ht₃, ht₄⟩ := exists_countable_locallyFinite_cover surjective_id hW₀ hW₁ hB

SphereEversion/Global/TwistOneJetSec.lean

@@ -159,10 +159,12 @@ theorem smooth_incl : Smooth ((I.prod 𝓘(𝕜, E →L[𝕜] V)).prod 𝓘(𝕜
     ContinuousLinearMap.id_comp]
   exact this.2
 
+omit [SmoothManifoldWithCorners I M] in
 @[simp]
 theorem incl_fst_fst (v : J¹[𝕜, E, I, M, V] × V) : (incl I M V v).1.1 = v.1.1 :=
   rfl
 
+omit [SmoothManifoldWithCorners I M] in
 @[simp]
 theorem incl_snd (v : J¹[𝕜, E, I, M, V] × V) : (incl I M V v).1.2 = v.2 :=
   rfl

SphereEversion/InductiveConstructions.lean

@@ -283,11 +283,11 @@ private theorem T_one : T 1 = 1 / 2 := by simp [T]
 
 private theorem T_pos {n : ℕ} (hn : n ≠ 0) : 0 < T n := by
   rw [T_eq, sub_pos]
-  apply pow_lt_one <;> first | assumption | norm_num
+  apply pow_lt_one₀ <;> first | assumption | norm_num
 
 private theorem T_nonneg (n : ℕ) : 0 ≤ T n := by
   rw [T_eq, sub_nonneg]
-  apply pow_le_one <;> norm_num
+  apply pow_le_one₀ <;> norm_num
 
 private theorem not_T_succ_le (n : ℕ) : ¬T (n + 1) ≤ 0 :=
   (T_pos n.succ_ne_zero).not_le

SphereEversion/Local/HPrinciple.lean

@@ -318,7 +318,7 @@ theorem bu_lt {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] (t : ℝ) (
       rw [norm_smul, Real.norm_eq_abs, abs_mul]
     _ ≤ ‖v‖ :=
       (mul_le_of_le_one_left (norm_nonneg _)
-        (mul_le_one (smoothStep.abs_le t) (abs_nonneg _) (L.ρ_le x)))
+        (mul_le_one₀ (smoothStep.abs_le t) (abs_nonneg _) (L.ρ_le x)))
     _ < ε := hv
 
 theorem improveStep_c0_close {ε : ℝ} (ε_pos : 0 < ε) :
@@ -433,8 +433,7 @@ section Improve
 This section proves `lem:h_principle_open_ample_loc`.
 -/
 
-
-open FiniteDimensional Submodule StepLandscape
+open Submodule StepLandscape
 
 variable {E}
 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] {R : RelLoc E F} (h_op : IsOpen R)
@@ -457,8 +456,8 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C
             (∀ x ∉ L.K₁, ∀ t, H t x = 𝓕 x) ∧
               (∀ x t, ‖(H t).f x - 𝓕.f x‖ ≤ ε) ∧
                 (∀ t, (H t).IsFormalSol R) ∧ ∀ᶠ x near L.K₀, (H 1).IsHolonomicAt x := by
-  let n := finrank ℝ E
-  let e := finBasis ℝ E
+  let n := Module.finrank ℝ E
+  let e := Module.finBasis ℝ E
   let E' := e.flag
   suffices
     ∀ k : Fin (n + 1),

SphereEversion/Local/SphereEversion.lean

@@ -23,7 +23,7 @@ proven in `Local/ParametricHPrinciple`.
 
 noncomputable section
 
-open Metric FiniteDimensional Set Function RelLoc InnerProductSpace Submodule
+open Metric Module Set Function RelLoc InnerProductSpace Submodule
 
 open Filter hiding mem_map
 
@@ -38,7 +38,7 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type*
 
 @[inherit_doc] local notation "𝕊²" => sphere (0 : E) 1
 
-@[inherit_doc] local notation "dim" => finrank ℝ
+@[inherit_doc] local notation "dim" => Module.finrank ℝ
 
 @[inherit_doc] local notation "pr[" x "]ᗮ" => projSpanOrthogonal x
 
@@ -432,7 +432,7 @@ theorem sphere_eversion_of_loc [Fact (dim E = 3)] :
   · exact fun t ht ↦ sphereImmersion_of_sol _ fun x hx ↦ h₃ x hx t ht
 
 -- Stating the full statement with all type-class arguments and no uncommon notation.
-example (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (finrank ℝ E = 3)] :
+example (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] :
     ∃ f : ℝ → E → E,
       ContDiff ℝ ⊤ (uncurry f) ∧
         (∀ x ∈ sphere (0 : E) 1, f 0 x = x) ∧

SphereEversion/Loops/Basic.lean

@@ -223,15 +223,15 @@ theorem _root_.Continuous.ofPath (x : X → Y) (t : X → ℝ) (γ : ∀ i, Path
   change Continuous fun i ↦ (fun s ↦ (γ s).extend) i (fract (t i))
   refine ContinuousOn.comp_fract ?_ ht ?_
   · have : Continuous (fun x : X × ℝ ↦ (x.1, projIcc 0 1 zero_le_one x.2)) :=
-      continuous_id.prod_map continuous_projIcc
+      continuous_id.prodMap continuous_projIcc
     exact (hγ.comp this).continuousOn
   · simp only [Icc.mk_zero, zero_le_one, Path.target, Path.extend_extends, imp_true_iff,
       eq_self_iff_true, Path.source, right_mem_Icc, left_mem_Icc, Icc.mk_one]
 
 /-- `Loop.ofPath` is continuous, where the endpoints of `γ` are fixed. TODO: remove -/
 theorem ofPath_continuous_family {x : Y} (γ : X → Path x x) (h : Continuous ↿γ) :
     Continuous ↿fun s ↦ ofPath <| γ s :=
-  Continuous.ofPath _ _ (fun i : X × ℝ ↦ γ i.1) (h.comp <| continuous_fst.prod_map continuous_id)
+  Continuous.ofPath _ _ (fun i : X × ℝ ↦ γ i.1) (h.comp <| continuous_fst.prodMap continuous_id)
     continuous_snd
 
 /-! ## Round trips -/

SphereEversion/Loops/Reparametrization.lean

@@ -47,13 +47,13 @@ existence of delta mollifiers, partitions of unity, and the inverse function the
 
 noncomputable section
 
-open Set Function MeasureTheory intervalIntegral Filter
+open Set Function MeasureTheory Module intervalIntegral Filter
 open scoped Topology Manifold
 
 variable {E F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
 set_option hygiene false
-notation "ι" => Fin (FiniteDimensional.finrank ℝ F + 1)
+notation "ι" => Fin (finrank ℝ F + 1)
 set_option hygiene true
 
 section MetricSpace

SphereEversion/Loops/Surrounding.lean

@@ -32,7 +32,7 @@ The key results are:
 -/
 
 -- to obtain that normed spaces are locally connected
-open Set Function FiniteDimensional Int Prod Path Filter
+open Set Function Module Int Prod Path Filter
 open scoped Topology unitInterval
 
 namespace IsPathConnected
@@ -259,7 +259,7 @@ section SurroundingPointsLimits
 
 variable {X Y : Type*} [FiniteDimensional ℝ F]
 
-local macro:arg "ι" : term => `(Fin (FiniteDimensional.finrank ℝ F + 1))
+local macro:arg "ι" : term => `(Fin (finrank ℝ F + 1))
 
 theorem eventually_surroundingPts_of_tendsto_of_tendsto {l : Filter X} {m : Filter Y} {v : ι → F}
     {q : F} {p : ι → X → F} {f : Y → F} (hq : ∃ w, SurroundingPts q v w)
@@ -271,7 +271,7 @@ theorem eventually_surroundingPts_of_tendsto_of_tendsto {l : Filter X} {m : Filt
   let W' : F × (ι → F) → ι → ℝ := uncurry (evalBarycentricCoords ι ℝ F)
   let A : Set (F × (ι → F)) := (univ : Set F) ×ˢ affineBases ι ℝ F
   let S : Set (F × (ι → F)) := W' ⁻¹' V
-  have hι : Fintype.card ι = FiniteDimensional.finrank ℝ F + 1 := Fintype.card_fin _
+  have hι : Fintype.card ι = finrank ℝ F + 1 := Fintype.card_fin _
   have hq' : v ∈ affineBases ι ℝ F := hw.mem_affineBases
   have hqv : (q, v) ∈ A := by simp [A, hq']
   have hxp : W' (q, v) ∈ V := by simp [W', V, hq', hw.coord_eq_w, hw.w_pos]
@@ -457,7 +457,7 @@ theorem surrounding_loop_of_convexHull [FiniteDimensional ℝ F] {f b : F} {O :
           (∀ s, γ 0 s = b) ∧
             (∀ s t, γ (projI t) s = γ t s) ∧ (∀ t s, γ t s ∈ O) ∧ (γ 1).Surrounds f := by
   rcases surrounded_of_convexHull O_op hsf with ⟨p, w, h, hp⟩
-  rw [← O_op.isConnected_iff_isPathConnected] at O_conn
+  rw [O_op.isConnected_iff_isPathConnected] at O_conn
   exact ⟨surroundingLoop O_conn hp hb, continuous_surroundingLoop, surroundingLoop_zero_right,
     surroundingLoop_zero_left, fun s t ↦ by rw [surroundingLoop_projI], surroundingLoop_mem,
     surroundingLoop_surrounds h⟩

SphereEversion/ToMathlib/Algebra/Periodic.lean

@@ -1,5 +1,5 @@
-import SphereEversion.ToMathlib.Topology.Separation
 import Mathlib.Analysis.Normed.Order.Lattice
+import SphereEversion.ToMathlib.Topology.Separation.Basic
 -- TODO: the file this references doesn't exist in mathlib any more; rename this one appropriately!
 
 /-!
@@ -101,11 +101,11 @@ theorem image_proj𝕊₁_Icc : proj𝕊₁ '' Icc 0 1 = univ :=
 theorem continuous_proj𝕊₁ : Continuous proj𝕊₁ :=
   continuous_quotient_mk'
 
-theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁ := QuotientAddGroup.isOpenMap_coe ℤSubℝ
+theorem isOpenMap_proj𝕊₁ : IsOpenMap proj𝕊₁ := QuotientAddGroup.isOpenMap_coe
 
 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𝕊₁)
+    IsQuotientMap fun p : X × ℝ ↦ (p.1, proj𝕊₁ p.2) :=
+  (IsOpenMap.id.prodMap isOpenMap_proj𝕊₁).isQuotientMap (continuous_id.prodMap continuous_proj𝕊₁)
     (surjective_id.prodMap Quotient.exists_rep)
 
 /-- A one-periodic function on `ℝ` descends to a function on the circle `ℝ ⧸ ℤ`. -/
@@ -120,7 +120,7 @@ instance : CompactSpace 𝕊₁ :=
   ⟨by rw [← image_proj𝕊₁_Icc]; exact isCompact_Icc.image continuous_proj𝕊₁⟩
 
 theorem isClosed_int : IsClosed (range ((↑) : ℤ → ℝ)) :=
-  Int.closedEmbedding_coe_real.isClosed_range
+  Int.isClosedEmbedding_coe_real.isClosed_range
 
 instance : T2Space 𝕊₁ := by
   have πcont : Continuous π := continuous_quotient_mk'
@@ -143,7 +143,7 @@ theorem Continuous.bounded_on_compact_of_onePeriodic {f : X → ℝ → E} (cont
     ∃ C, ∀ x ∈ K, ∀ t, ‖f x t‖ ≤ C := by
   let F : X × 𝕊₁ → E := fun p : X × 𝕊₁ ↦ (hper p.1).lift p.2
   have Fcont : Continuous F := by
-    have qm : QuotientMap fun p : X × ℝ ↦ (p.1, π p.2) := quotientMap_id_proj𝕊₁
+    have qm : IsQuotientMap fun p : X × ℝ ↦ (p.1, π p.2) := quotientMap_id_proj𝕊₁
     -- avoid weird elaboration issue
     have : ↿f = F ∘ fun p : X × ℝ ↦ (p.1, π p.2) := by ext p; rfl
     rwa [this, ← qm.continuous_iff] at cont

SphereEversion/ToMathlib/Analysis/Calculus.lean

@@ -25,16 +25,6 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCom
   [NormedSpace 𝕜 E'] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*}
   [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ∞}
 
-theorem ContDiffAt.comp₂ {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {x : F}
-    (hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x)) (hf₁ : ContDiffAt 𝕜 n f₁ x) (hf₂ : ContDiffAt 𝕜 n f₂ x) :
-    ContDiffAt 𝕜 n (fun x ↦ g (f₁ x, f₂ x)) x :=
-  hg.comp x <| hf₁.prod hf₂
-
-theorem ContDiffAt.clm_comp {g : E' → F →L[𝕜] G} {f : E' → E →L[𝕜] F} {n : ℕ∞} {x : E'}
-    (hg : ContDiffAt 𝕜 n g x) (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun x ↦ g x ∘L f x) x :=
-  isBoundedBilinearMap_comp.contDiff.contDiffAt.comp₂
-    (g := fun p => ContinuousLinearMap.comp p.1 p.2) hg hf
-
 theorem fderiv_prod_left {x₀ : E} {y₀ : F} :
     fderiv 𝕜 (fun x ↦ (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 E F :=
   ((hasFDerivAt_id _).prod (hasFDerivAt_const _ _)).fderiv

SphereEversion/ToMathlib/Analysis/InnerProductSpace/CrossProduct.lean

@@ -10,12 +10,11 @@ import Mathlib.Analysis.InnerProductSpace.Orientation
 
 /-! # The cross-product on an oriented real inner product space of dimension three -/
 
-
 noncomputable section
 
 open scoped RealInnerProductSpace
 
-open FiniteDimensional
+open Module
 
 set_option synthInstance.checkSynthOrder false
 attribute [local instance] FiniteDimensional.of_fact_finrank_eq_succ
@@ -95,7 +94,7 @@ theorem norm_crossProduct (u : E) (v : (ℝ ∙ u)ᗮ) : ‖u×₃v‖ = ‖u‖
         ω.volumeForm_apply_le ![u, v, u×₃v]
   let K : Submodule ℝ E := Submodule.span ℝ ({u, ↑v} : Set E)
   have : Nontrivial Kᗮ := by
-    apply FiniteDimensional.nontrivial_of_finrank_pos (R := ℝ)
+    apply Module.nontrivial_of_finrank_pos (R := ℝ)
     have : finrank ℝ K ≤ Finset.card {u, (v : E)} := by
       simpa [Set.toFinset_singleton] using finrank_span_le_card ({u, ↑v} : Set E)
     have : Finset.card {u, (v : E)} ≤ Finset.card {(v : E)} + 1 := Finset.card_insert_le u {↑v}

SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean

@@ -16,7 +16,7 @@ noncomputable section
 
 open scoped RealInnerProductSpace
 
-open FiniteDimensional
+open Module
 
 set_option synthInstance.checkSynthOrder false
 attribute [local instance] FiniteDimensional.of_fact_finrank_eq_succ

SphereEversion/ToMathlib/ExistsOfConvex.lean

@@ -89,7 +89,7 @@ theorem exists_contMDiff_of_convex {P : M → F → Prop} (hP : ∀ x, Convex 
   have hPP' : ∀ x, ∃ f : M → F, ∀ᶠ x' in 𝓝 x, PP ⟨x', f⟩ := fun x ↦ by
     rcases hP' x with ⟨U, U_in, f, hf, hf'⟩
     use f
-    filter_upwards [eventually_mem_nhds.mpr U_in] with y hy
+    filter_upwards [eventually_mem_nhds_iff.mpr U_in] with y hy
     exact ⟨hf.contMDiffAt hy, hf' y (mem_of_mem_nhds hy)⟩
   rcases exists_of_convex hPP hPP' with ⟨f, hf⟩
   exact ⟨f, fun x ↦ (hf x).1, fun x ↦ (hf x).2⟩
@@ -159,7 +159,7 @@ theorem exists_contMDiff_of_convex₂ {P : M₁ → (M₂ → F) → Prop} [Sigm
   have hPP' : ∀ x, ∃ f : M₁ → M₂ → F, ∀ᶠ x' in 𝓝 x, PP ⟨x', f⟩ := fun x ↦ by
     rcases hP' x with ⟨U, U_in, f, hf, hf'⟩
     use f
-    filter_upwards [eventually_mem_nhds.mpr U_in] with y hy
+    filter_upwards [eventually_mem_nhds_iff.mpr U_in] with y hy
     exact ⟨fun z ↦ hf.contMDiffAt (prod_mem_nhds hy univ_mem), hf' y (mem_of_mem_nhds hy)⟩
   rcases exists_of_convex hPP hPP' with ⟨f, hf⟩
   exact ⟨f, fun ⟨x, y⟩ ↦ (hf x).1 y, fun x ↦ (hf x).2⟩

SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Michael Rothgang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Rothgang
 -/
+import Mathlib.Geometry.Manifold.ContMDiff.Defs
 import Mathlib.Geometry.Manifold.MFDeriv.Defs
 
 /-! ## Smooth immersions