fix

SphereEversion.lean

@@ -57,9 +57,8 @@ import SphereEversion.ToMathlib.Order.Filter.Basic
 import SphereEversion.ToMathlib.Partition
 import SphereEversion.ToMathlib.SmoothBarycentric
 import SphereEversion.ToMathlib.Topology.Algebra.Module
-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.Basic
+import SphereEversion.ToMathlib.Topology.Separation.Hausdorff
 import SphereEversion.ToMathlib.Unused.Fin

SphereEversion/Global/Gromov.lean

@@ -14,19 +14,17 @@ noncomputable section
 
 open Set Filter ModelWithCorners Metric
 
-open scoped Topology Manifold
-
-local notation "∞" => (⊤ : ℕ∞)
+open scoped Topology Manifold ContDiff
 
 variable {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimensional ℝ EM]
   {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} [Boundaryless IM]
-  {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M]
+  {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM ∞ M]
   [T2Space M] [SigmaCompactSpace M]
   {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [FiniteDimensional ℝ EX]
   {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} [Boundaryless IX]
   -- note: X is a metric space
   {X : Type*}
-  [MetricSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners IX X] [SigmaCompactSpace X]
+  [MetricSpace X] [ChartedSpace HX X] [IsManifold IX ∞ X] [SigmaCompactSpace X]
   {R : RelMfld IM M IX X} {A : Set M} {δ : M → ℝ}
 
 @[inherit_doc] local notation "J¹" => OneJetBundle IM M IX X
@@ -312,7 +310,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R
           _ = τ x := by simp [F, η]
     · rw [union_assoc, Eventually.union_nhdsSet] at hF'hol
       replace hF'hol := hF'hol.2
-      simp_rw [← L.iUnion_succ'] at hF'hol
+      simp_rw [L.iUnion_succ']
       exact hF'hol
     · exact F'.smooth
     · intro t x hx
@@ -342,7 +340,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R
 
 variable {EP : Type*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] [FiniteDimensional ℝ EP]
   {HP : Type*} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} [Boundaryless IP]
-  {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] [SmoothManifoldWithCorners IP P]
+  {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP ∞ P]
   [SigmaCompactSpace P] [T2Space P] {C : Set (P × M)}
 
 /-
@@ -364,7 +362,7 @@ theorem RelMfld.Ample.satisfiesHPrincipleWith (hRample : R.Ample) (hRopen : IsOp
 variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E']
   {H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [I'.Boundaryless]
   {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
-  [SmoothManifoldWithCorners I' M'] [SigmaCompactSpace M'] [T2Space M']
+  [IsManifold I' ∞ M'] [SigmaCompactSpace M'] [T2Space M']
 
 /-
 Since every (σ-compact) manifold is metrizable, the metric space assumption can be removed.

SphereEversion/Global/Immersion.lean

@@ -13,19 +13,20 @@ open Metric Module Set Function LinearMap Filter ContinuousLinearMap
 
 open scoped Manifold Topology
 
-local notation "∞" => (⊤ : ℕ∞)
+-- Can't open ContDiff because `ω` conflicts with the notation for orientation below
+local notation "∞" => ((⊤ : ℕ∞) : WithTop ℕ∞)
 
 section General
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type*} [TopologicalSpace M]
-  [ChartedSpace H M] [SmoothManifoldWithCorners I M]
+  [ChartedSpace H M] [IsManifold I ∞ M]
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E']
   {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H')
-  {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M']
+  {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M']
   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type*} [TopologicalSpace G]
   (J : ModelWithCorners ℝ F G)
-  (N : Type*) [TopologicalSpace N] [ChartedSpace G N] [SmoothManifoldWithCorners J N]
+  (N : Type*) [TopologicalSpace N] [ChartedSpace G N] [IsManifold J ∞ N]
 
 @[inherit_doc] local notation "TM" => TangentSpace I
 @[inherit_doc] local notation "TM'" => TangentSpace I'
@@ -37,7 +38,7 @@ variable (M M') in
 def immersionRel : RelMfld I M I' M' :=
   {σ | Injective σ.2}
 
-omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
+omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 @[simp]
 theorem mem_immersionRel_iff {σ : OneJetBundle I M I' M'} :
     σ ∈ immersionRel I M I' M' ↔ Injective (σ.2 : TangentSpace I _ →L[ℝ] TangentSpace I' _) :=
@@ -67,7 +68,7 @@ theorem immersionRel_open [FiniteDimensional ℝ E] : IsOpen (immersionRel I M I
   · infer_instance
   · infer_instance
 
-omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
+omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 @[simp]
 theorem immersionRel_slice_eq {m : M} {m' : M'} {p : DualPair <| TangentSpace I m}
     {φ : TangentSpace I m →L[ℝ] TangentSpace I' m'} (hφ : Injective φ) :
@@ -76,7 +77,7 @@ theorem immersionRel_slice_eq {m : M} {m' : M'} {p : DualPair <| TangentSpace I
 
 variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ E']
 
-omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
+omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem immersionRel_ample (h : finrank ℝ E < finrank ℝ E') : (immersionRel I M I' M').Ample := by
   rw [RelMfld.ample_iff]
   rintro ⟨⟨m, m'⟩, φ : TangentSpace I m →L[ℝ] TangentSpace I' m'⟩ (p : DualPair (TangentSpace I m))
@@ -97,13 +98,13 @@ section Generalbis
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
   {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless]
-  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M]
+  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E']
   {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless]
-  {M' : Type*} [MetricSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M']
+  {M' : Type*} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M']
   {EP : Type*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] [FiniteDimensional ℝ EP]
   {HP : Type*} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} [IP.Boundaryless]
-  {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] [SmoothManifoldWithCorners IP P]
+  {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP ∞ P]
   {C : Set (P × M)} {ε : M → ℝ}
 
 variable (M M' IP P)
@@ -125,17 +126,17 @@ variable {n : ℕ} (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 
 /-- The inclusion of `𝕊^n` into `ℝ^{n+1}` is an immersion. -/
 theorem immersion_inclusion_sphere : Immersion (𝓡 n) 𝓘(ℝ, E)
-    (fun x : sphere (0 : E) 1 ↦ (x : E)) ⊤ where
-  contMDiff := contMDiff_coe_sphere
+    (fun x : sphere (0 : E) 1 ↦ (x : E)) ∞ where
+  contMDiff := contMDiff_coe_sphere.of_le le_top
   diff_injective := mfderiv_coe_sphere_injective
 
 /-- The antipodal map on `𝕊^n ⊆ ℝ^{n+1}` is an immersion. -/
 theorem immersion_antipodal_sphere : Immersion (𝓡 n) 𝓘(ℝ, E)
-    (fun x : sphere (0 : E) 1 ↦ -(x : E)) ⊤ where
+    (fun x : sphere (0 : E) 1 ↦ -(x : E)) ∞ where
   contMDiff :=
     -- Write this as the composition of `coe_sphere` and the antipodal map on `E`.
     -- The other direction elaborates much worse.
-    (contDiff_neg.contMDiff).comp contMDiff_coe_sphere
+    (contDiff_neg.contMDiff).comp (contMDiff_coe_sphere.of_le le_top)
   diff_injective x := by
     change Injective (mfderiv (𝓡 n) 𝓘(ℝ, E) (-fun x : sphere (0 : E) 1 ↦ (x : E)) x)
     rw [mfderiv_neg]
@@ -167,20 +168,20 @@ theorem smooth_bs :
       fun p : ℝ × (sphere (0 : E) 1) ↦ (1 - p.1) • (p.2 : E) + p.1 • -(p.2: E) := by
   refine (ContMDiff.smul ?_ ?_).add (contMDiff_fst.smul ?_)
   · exact (contDiff_const.sub contDiff_id).contMDiff.comp contMDiff_fst
-  · exact contMDiff_coe_sphere.comp contMDiff_snd
-  · exact (contDiff_neg.contMDiff.comp contMDiff_coe_sphere).comp contMDiff_snd
+  · exact (contMDiff_coe_sphere.of_le le_top).comp contMDiff_snd
+  · exact (contDiff_neg.contMDiff.comp (contMDiff_coe_sphere.of_le le_top)).comp contMDiff_snd
 
 def formalEversionAux : FamilyOneJetSec (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ, ℝ) ℝ :=
   familyJoin (smooth_bs E) <|
-    familyTwist (drop (oneJetExtSec ⟨((↑) : 𝕊² → E), contMDiff_coe_sphere⟩))
+    familyTwist (drop (oneJetExtSec ⟨((↑) : 𝕊² → E), contMDiff_coe_sphere.of_le le_top⟩))
       (fun p : ℝ × 𝕊² ↦ ω.rot (p.1, p.2))
       (by
         intro p
         have : ContMDiffAt 𝓘(ℝ, ℝ × E) 𝓘(ℝ, E →L[ℝ] E) ∞ ω.rot (p.1, p.2) := by
           refine ((ω.contDiff_rot ?_).of_le le_top).contMDiffAt
           exact ne_zero_of_mem_unit_sphere p.2
         apply this.comp p (f := fun (p : ℝ × sphere 0 1) ↦ (p.1, (p.2 : E)))
-        apply contMDiff_fst.prod_mk_space (contMDiff_coe_sphere.comp contMDiff_snd))
+        apply contMDiff_fst.prod_mk_space ((contMDiff_coe_sphere.of_le le_top).comp contMDiff_snd))
 
 /-- A formal eversion of a two-sphere into its ambient Euclidean space. -/
 def formalEversionAux2 : HtpyFormalSol 𝓡_imm :=
@@ -309,7 +310,7 @@ theorem sphere_eversion :
     ∃ f : ℝ → 𝕊² → E,
       ContMDiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E) ∞ ↿f ∧
         (f 0 = fun x : 𝕊² ↦ (x : E)) ∧ (f 1 = fun x : 𝕊² ↦ -(x : E)) ∧
-        ∀ t, Immersion (𝓡 2) 𝓘(ℝ, E) (f t) ⊤ := by
+        ∀ t, Immersion (𝓡 2) 𝓘(ℝ, E) (f t) ∞ := by
   classical
   let ω : Orientation ℝ E (Fin 3) :=
     ((stdOrthonormalBasis _ _).reindex <|

SphereEversion/Global/Localisation.lean

@@ -11,7 +11,7 @@ is about embedding any manifold into another one).
 
 noncomputable section
 
-open scoped Topology Manifold
+open scoped Topology Manifold ContDiff
 open Set ContinuousLinearMap
 
 section Loc
@@ -112,10 +112,10 @@ end Unloc
 universe u₁ u₂ u₃ u₄ u₅ u₆
 variable {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {H : Type u₂} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
-  (M : Type u₃) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M]
+  (M : Type u₃) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
   {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E']
   {H' : Type u₅} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H')
-  (M' : Type u₆) [MetricSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M']
+  (M' : Type u₆) [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M']
   {R : RelMfld I M I' M'}
 
 /-- A pair of charts together with a compact subset of the first vector space. -/
@@ -147,7 +147,7 @@ structure ChartPair.compat' (F : FormalSol R) (𝓕 : (R.localize p.φ p.ψ).rel
 def RelLoc.HtpyFormalSol.unloc : _root_.HtpyFormalSol (RelMfld.localize p.φ p.ψ R) :=
   { 𝓕.toHtpyJetSec.unloc with is_sol' := 𝓕.is_sol }
 
-omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
+omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem RelLoc.HtpyFormalSol.unloc_congr {𝓕 𝓕' : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {t t' x}
     (h : 𝓕 t x = 𝓕' t' x) : 𝓕.unloc p t x = 𝓕'.unloc p t' x := by
   ext1
@@ -157,7 +157,7 @@ theorem RelLoc.HtpyFormalSol.unloc_congr {𝓕 𝓕' : (R.localize p.φ p.ψ).re
   · change (𝓕 t x).2 = (𝓕' t' x).2
     rw [h]
 
-omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
+omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem RelLoc.HtpyFormalSol.unloc_congr_const {𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol}
     {𝓕' : (R.localize p.φ p.ψ).relLoc.FormalSol} {t x} (h : 𝓕 t x = 𝓕' x) :
     𝓕.unloc p t x = 𝓕'.unloc x := by
@@ -168,7 +168,7 @@ theorem RelLoc.HtpyFormalSol.unloc_congr_const {𝓕 : (R.localize p.φ p.ψ).re
   · change (𝓕 t x).2 = (𝓕' x).2
     rw [h]
 
-omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
+omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem RelLoc.HtpyFormalSol.unloc_congr' {𝓕 𝓕' : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {t t'}
     (h : 𝓕 t = 𝓕' t') : 𝓕.unloc p t = 𝓕'.unloc p t' := by
   apply FormalSol.coe_inj

SphereEversion/Global/LocalisationData.lean

@@ -3,7 +3,7 @@ import SphereEversion.Global.SmoothEmbedding
 
 noncomputable section
 
-open scoped Manifold
+open scoped Manifold ContDiff
 
 open Set Metric
 
@@ -12,10 +12,10 @@ section
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
   {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
-  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M]
+  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
   {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
-  {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M']
+  {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M']
 
 /-- Definition `def:localisation_data`. -/
 structure LocalisationData (f : M → M') where
@@ -44,7 +44,7 @@ abbrev ψj : IndexType ld.N → OpenSmoothEmbedding 𝓘(𝕜, E') E' I' M' :=
 def ι (L : LocalisationData I I' f) :=
   IndexType L.N
 
-omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
+omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in
 theorem iUnion_succ' {β : Type*} (s : ld.ι → Set β) (i : IndexType ld.N) :
     (⋃ j ≤ i, s j) = (⋃ j < i, s j) ∪ s i := by
   simp only [(fun _ ↦ le_iff_lt_or_eq : ∀ j, j ≤ i ↔ j < i ∨ j = i)]
@@ -64,11 +64,11 @@ open ModelWithCorners
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
   {M : Type*} [TopologicalSpace M] [SigmaCompactSpace M] [LocallyCompactSpace M] [T2Space M]
   {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [Boundaryless I] [Nonempty M]
-  [ChartedSpace H M] [SmoothManifoldWithCorners I M]
+  [ChartedSpace H M] [IsManifold I ∞ M]
   (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E']
   {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [Boundaryless I']
   {M' : Type*} [MetricSpace M'] [SigmaCompactSpace M'] [LocallyCompactSpace M']
-  [Nonempty M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M']
+  [Nonempty M'] [ChartedSpace H' M'] [IsManifold I' ∞ M']
 
 variable (M')
 
@@ -124,8 +124,8 @@ variable {E E' I I'}
 section
 
 omit [FiniteDimensional ℝ E] [SigmaCompactSpace M] [LocallyCompactSpace M] [T2Space M]
-  [I.Boundaryless] [Nonempty M] [SmoothManifoldWithCorners I M] [I'.Boundaryless]
-  [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [SmoothManifoldWithCorners I' M']
+  [I.Boundaryless] [Nonempty M] [IsManifold I ∞ M] [I'.Boundaryless]
+  [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [IsManifold I' ∞ M']
 
 /-- Lemma `lem:localisation_stability`. -/
 theorem localisation_stability {f : M → M'} (ld : LocalisationData I I' f) :

SphereEversion/Global/LocalizedConstruction.lean

@@ -5,15 +5,15 @@ noncomputable section
 
 open Set Filter ModelWithCorners Metric
 
-open scoped Topology Manifold
+open scoped Topology Manifold ContDiff
 
 variable {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimensional ℝ EM]
   {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM}
-  {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M]
+  {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM ∞ M]
   [T2Space M]
   {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [FiniteDimensional ℝ EX]
   {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX}
-  {X : Type*} [MetricSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners IX X]
+  {X : Type*} [MetricSpace X] [ChartedSpace HX X] [IsManifold IX ∞ X]
 
 theorem OpenSmoothEmbedding.improve_formalSol (φ : OpenSmoothEmbedding 𝓘(ℝ, EM) EM IM M)
     (ψ : OpenSmoothEmbedding 𝓘(ℝ, EX) EX IX X) {R : RelMfld IM M IX X} (hRample : R.Ample)