Merge pull request #87 from Ruben-VandeVelde/MR-bump-4.12

Bump to v4.12.0

Author: grunweg

SphereEversion/Global/Immersion.lean

@@ -53,9 +53,7 @@ theorem chartAt_image_immersionRel_eq {σ : OneJetBundle I M I' M'} :
     ψJ σ '' ((ψJ σ).source ∩ immersionRel I M I' M') = (ψJ σ).target ∩ {q : HJ | Injective q.2} :=
   PartialEquiv.IsImage.image_eq fun _σ' hσ' ↦ (mem_immersionRel_iff' I I' hσ').symm
 
-variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ E']
-
-theorem immersionRel_open : IsOpen (immersionRel I M I' M') := by
+theorem immersionRel_open [FiniteDimensional ℝ E] : IsOpen (immersionRel I M I' M') := by
   simp_rw [ChartedSpace.isOpen_iff HJ (immersionRel I M I' M'), chartAt_image_immersionRel_eq]
   refine fun σ ↦ (ψJ σ).open_target.inter ?_
   convert isOpen_univ.prod ContinuousLinearMap.isOpen_injective
@@ -72,6 +70,8 @@ theorem immersionRel_slice_eq {m : M} {m' : M'} {p : DualPair <| TangentSpace I
     (immersionRel I M I' M').slice ⟨(m, m'), φ⟩ p = ((ker p.π).map φ : Set <| TM' m')ᶜ :=
   Set.ext_iff.mpr fun _ ↦ p.injective_update_iff hφ
 
+variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ E']
+
 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))
@@ -96,7 +96,6 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimension
   {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']
-  [FiniteDimensional ℝ E] [FiniteDimensional ℝ E']
   {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]
@@ -274,13 +273,13 @@ theorem ContDiff.uncurry_left {f : E → F → G} (n : ℕ∞) (hf : ContDiff 
 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]
   {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
   {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
-  {M' : Type*} [MetricSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M']
+  {M' : Type*} [MetricSpace M'] [ChartedSpace H' M']
   {EP : Type*} [NormedAddCommGroup EP] [NormedSpace 𝕜 EP]
   {HP : Type*} [TopologicalSpace HP] (IP : ModelWithCorners 𝕜 EP HP)
-  {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] [SmoothManifoldWithCorners IP P]
+  {P : Type*} [TopologicalSpace P] [ChartedSpace HP P]
 
 -- move to Mathlib.Geometry.Manifold.ContMDiff.Product
 lemma Smooth.inr (x : M) :

SphereEversion/Global/Localisation.lean

@@ -178,14 +178,14 @@ theorem FormalSol.transfer_unloc_localize (F : FormalSol R) (hF : range (F.bs 
 
 open scoped Classical
 
-variable [T2Space M]
-
 lemma ChartPair.mkHtpy_aux {F : FormalSol R} {𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol}
     (h : p.compat' F 𝓕) (t x) (hx : x ∉ p.K₁) :
     F (p.φ x) = OneJetBundle.embedding p.φ p.ψ (RelLoc.HtpyFormalSol.unloc p 𝓕 t x) := by
   rw [← F.transfer_unloc_localize p h.1, RelLoc.HtpyFormalSol.unloc_congr_const p (h.hFF x hx t)]
   rfl
 
+variable [T2Space M]
+
 def ChartPair.mkHtpy (F : FormalSol R) (𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol) :
     HtpyFormalSol R :=
   if h : p.compat' F 𝓕 then
@@ -261,7 +261,7 @@ theorem ChartPair.mkHtpy_isHolonomicAt_iff {F : FormalSol R}
     rw [p.φ.updateFormalSol_bs p.ψ p.hK₁]
     simp only [Function.comp_apply, OpenSmoothEmbedding.update_apply_embedding, mem_range_self]
   rw [← isHolonomicAt_localize_iff _ p.φ p.ψ rg e, ← JetSec.unloc_hol_at_iff]
-  exact OneJetSec.isHolonomicAt_congr (Filter.eventually_of_forall fun e ↦ p.mkHtpy_localize h rg)
+  exact OneJetSec.isHolonomicAt_congr (Filter.Eventually.of_forall fun e ↦ p.mkHtpy_localize h rg)
 
 theorem ChartPair.dist_update' [FiniteDimensional ℝ E'] {δ : M → ℝ} (hδ_pos : ∀ x, 0 < δ x)
     (hδ_cont : Continuous δ) {F : FormalSol R} (hF : range (F.bs ∘ p.φ) ⊆ range p.ψ) :

SphereEversion/Global/LocalisationData.lean

@@ -44,6 +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
 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)]
@@ -90,6 +91,7 @@ theorem targetCharts_cover : (⋃ i', targetCharts E' I' M' i' '' ball (0 : E')
 variable (E) {M'}
 variable {f : M → M'} (hf : Continuous f)
 
+include hf in
 theorem nice_atlas_domain :
     ∃ n,
       ∃ φ : IndexType n → OpenSmoothEmbedding 𝓘(ℝ, E) E I M,
@@ -119,6 +121,12 @@ def stdLocalisationData : LocalisationData I I' f where
 
 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']
+
 /-- Lemma `lem:localisation_stability`. -/
 theorem localisation_stability {f : M → M'} (ld : LocalisationData I I' f) :
     ∃ (ε : M → ℝ) (_hε : ∀ m, 0 < ε m) (_hε' : Continuous ε),
@@ -154,8 +162,12 @@ theorem ε_spec (ld : LocalisationData I I' f) :
       range (g ∘ ld.φ i) ⊆ range (ld.ψj i) :=
   (localisation_stability ld).choose_spec.choose_spec.choose_spec
 
+end LocalisationData
+end
+
 variable (I I')
 
+open LocalisationData in
 theorem _root_.exists_stability_dist {f : M → M'} (hf : Continuous f) :
     ∃ ε : M → ℝ, (∀ m, 0 < ε m) ∧ Continuous ε ∧
       ∀ x : M,
@@ -171,6 +183,4 @@ theorem _root_.exists_stability_dist {f : M → M'} (hf : Continuous f) :
   have := L.ε_spec
   tauto
 
-end LocalisationData
-
 end

SphereEversion/Global/LocalizedConstruction.lean

@@ -8,16 +8,12 @@ open Set Filter ModelWithCorners Metric
 open scoped Topology Manifold
 
 variable {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimensional ℝ EM]
-  {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} [Boundaryless IM]
+  {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM}
   {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M]
-  [T2Space M] [LocallyCompactSpace M] [Nonempty M] [SigmaCompactSpace M]
+  [T2Space M]
   {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [FiniteDimensional ℝ EX]
-  [MeasurableSpace EX] [BorelSpace 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] [LocallyCompactSpace X]
-  [SigmaCompactSpace X] [Nonempty X]
+  {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX}
+  {X : Type*} [MetricSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners 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)
@@ -73,7 +69,7 @@ theorem OpenSmoothEmbedding.improve_formalSol (φ : OpenSmoothEmbedding 𝓘(ℝ
     exact p.mkHtpy_eq_of_forall hcompat ht
   have hF't1 : ∀ᶠ t : ℝ near Ici 1, F' t = F' 1 := h𝓕't1.mono fun t ↦ p.mkHtpy_congr _
   refine ⟨F', hF't0, hF't1, ?_, hF'relK₁, ?_, ?_⟩
-  · apply φ.forall_near hK₁ h𝓕'relC (eventually_of_forall fun x hx t ↦ hF'relK₁ t x hx)
+  · apply φ.forall_near hK₁ h𝓕'relC (Eventually.of_forall fun x hx t ↦ hF'relK₁ t x hx)
     · intro e he t
       rw [p.mkHtpy_eq_of_eq _ _ hcompat]
       exact he t

SphereEversion/Global/OneJetBundle.lean

@@ -13,6 +13,7 @@ import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
 import Mathlib.Geometry.Manifold.VectorBundle.Hom
 import Mathlib.Geometry.Manifold.VectorBundle.Pullback
+import Mathlib.Tactic.Monotonicity.Lemmas
 
 /-!
 # 1-jet bundles
@@ -48,7 +49,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M''] [SmoothManifoldWithCorners 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]
   {F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕜 F']
   {G' : Type*} [TopologicalSpace G'] (J' : ModelWithCorners 𝕜 F' G')
   {N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N'] [SmoothManifoldWithCorners J' N']
@@ -294,8 +295,6 @@ lemma ContMDiffMap.snd_apply (x : M) (x' : M') :
 
 end
 
-attribute [gcongr] preimage_mono Set.prod_mono
-
 /-- In `J¹(M, M')`, the target of a chart has a nice formula -/
 theorem oneJetBundle_chart_target (x₀ : J¹MM') :
     (chartAt HJ x₀).target = Prod.fst ⁻¹' (chartAt (ModelProd H H') x₀.proj).target := by
@@ -415,6 +414,9 @@ theorem SmoothAt.clm_comp_inTangentCoordinates {f : N → M} {g : N → M'} {h :
 
 variable (I')
 
+variable [SmoothManifoldWithCorners J N]
+
+omit [SmoothManifoldWithCorners J' N'] in
 theorem SmoothAt.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} {x₀ : N'}
     {h : ∀ x : N', OneJetSpace I' J (f2 x, f3 x)} {g : ∀ x : N', OneJetSpace I I' (f1 x, f2 x)}
     (hh : SmoothAt J' ((I'.prod J).prod 𝓘(𝕜, E' →L[𝕜] F)) (fun x ↦ OneJetBundle.mk _ _ (h x)) x₀)
@@ -424,6 +426,7 @@ theorem SmoothAt.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} {x
   rw [smoothAt_oneJetBundle_mk] at hh hg ⊢
   exact ⟨hg.1, hh.2.1, hh.2.2.clm_comp_inTangentCoordinates hg.2.1.continuousAt hg.2.2⟩
 
+omit [SmoothManifoldWithCorners J' N'] in
 theorem Smooth.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N}
     {h : ∀ x : N', OneJetSpace I' J (f2 x, f3 x)} {g : ∀ x : N', OneJetSpace I I' (f1 x, f2 x)}
     (hh : Smooth J' ((I'.prod J).prod 𝓘(𝕜, E' →L[𝕜] F)) fun x ↦ OneJetBundle.mk _ _ (h x))
@@ -435,6 +438,7 @@ theorem Smooth.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N}
 variable {I'}
 
 open Trivialization in
+omit [SmoothManifoldWithCorners J N] in
 theorem Smooth.oneJet_add {f : N → M} {g : N → M'} {ϕ ϕ' : ∀ x : N, OneJetSpace I I' (f x, g x)}
     (hϕ : Smooth J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) fun x ↦ OneJetBundle.mk _ _ (ϕ x))
     (hϕ' : Smooth J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) fun x ↦ OneJetBundle.mk _ _ (ϕ' x)) :

SphereEversion/Global/OneJetSec.lean

@@ -104,7 +104,7 @@ its base map at x. -/
 theorem isHolonomicAt_iff {F : OneJetSec I M I' M'} {x : M} :
     F.IsHolonomicAt x ↔ oneJetExt I I' F.bs x = F x := by
   simp_rw [IsHolonomicAt, oneJetExt, Bundle.TotalSpace.ext_iff, heq_iff_eq, F.fst_eq,
-    oneJetBundle_mk_fst, true_and_iff, oneJetBundle_mk_snd]
+    oneJetBundle_mk_fst, true_and, oneJetBundle_mk_snd]
 
 theorem isHolonomicAt_congr {F F' : OneJetSec I M I' M'} {x : M} (h : F =ᶠ[𝓝 x] F') :
     F.IsHolonomicAt x ↔ F'.IsHolonomicAt x := by
@@ -161,7 +161,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top
   [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners 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] {F' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F']
+  {F' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F']
   {G' : Type*} [TopologicalSpace G'] (J' : ModelWithCorners ℝ F' G') (N' : Type*)
   [TopologicalSpace N'] [ChartedSpace G' N'] [SmoothManifoldWithCorners J' N'] {EP : Type*}
   [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type*} [TopologicalSpace HP]

SphereEversion/Global/ParametricityForFree.lean

@@ -131,7 +131,7 @@ theorem RelMfld.Ample.relativize (hR : R.Ample) : (R.relativize IP P).Ample := b
   obtain ⟨u', hu'⟩ := ContinuousLinearMap.exists_ne_zero h
   let u := (p2 u')⁻¹ • u'
   let q : DualPair (TangentSpace I σ.1.1.2) :=
-    ⟨p2, u, by erw [p2.map_smul, smul_eq_mul, inv_mul_cancel hu']⟩
+    ⟨p2, u, by erw [p2.map_smul, smul_eq_mul, inv_mul_cancel₀ hu']⟩
   rw [relativize_slice q rfl]
   exact (hR q).vadd
 

SphereEversion/Global/Relation.lean

@@ -40,13 +40,13 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners 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]
   {F' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F']
   {G' : Type*} [TopologicalSpace G'] (J' : ModelWithCorners ℝ F' G')
   (N' : Type*) [TopologicalSpace N'] [ChartedSpace G' N'] [SmoothManifoldWithCorners J' N']
   {EP : Type*} [NormedAddCommGroup EP] [NormedSpace ℝ EP]
   {HP : Type*} [TopologicalSpace HP] (IP : ModelWithCorners ℝ EP HP)
-  (P : Type*) [TopologicalSpace P] [ChartedSpace HP P] [SmoothManifoldWithCorners IP P]
+  (P : Type*) [TopologicalSpace P] [ChartedSpace HP P]
   {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX]
   {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX}
   -- note: X is a metric space
@@ -74,7 +74,7 @@ instance (R : RelMfld I M I' M') : FunLike (FormalSol R) M (OneJetBundle I M I'
     intro F G h
     ext x : 2
     · exact congrArg Prod.snd (congrArg Bundle.TotalSpace.proj (congrFun h x))
-    · simpa using ((Bundle.TotalSpace.ext_iff _ _).mp (congrFun h x)).2
+    · simpa using (Bundle.TotalSpace.ext_iff.mp (congrFun h x)).2
 
 
 def mkFormalSol (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x) (hsol : ∀ x, F x ∈ R)

SphereEversion/Global/SmoothEmbedding.lean

@@ -17,10 +17,9 @@ section General
 
 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] {E' : Type*}
-  [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H']
+  [TopologicalSpace M] [ChartedSpace H 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']
 
 structure OpenSmoothEmbedding where
   toFun : M → M'
@@ -79,6 +78,10 @@ theorem isOpenMap : IsOpenMap f :=
 theorem coe_comp_invFun_eventuallyEq (x : M) : f ∘ f.invFun =ᶠ[𝓝 (f x)] id :=
   Filter.eventually_of_mem (f.isOpenMap.range_mem_nhds x) fun _ hy ↦ f.right_inv hy
 
+section
+
+variable [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
+
 /- Note that we are slightly abusing the fact that `TangentSpace I x` and
 `TangentSpace I (f.invFun (f x))` are both definitionally `E` below. -/
 def fderiv (x : M) : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x) :=
@@ -116,6 +119,8 @@ theorem fderiv_symm_coe' {x : M'} (hx : x ∈ range f) :
       (mfderiv I' I f.invFun x : TangentSpace I' x →L[𝕜] TangentSpace I (f.invFun x)) :=
   by rw [fderiv_symm_coe, f.right_inv hx]
 
+end
+
 open Filter
 
 theorem openEmbedding : OpenEmbedding f :=
@@ -227,7 +232,7 @@ open Function
 universe u
 
 variable {F H : Type*} (M : Type u) [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H]
-  [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [LocallyCompactSpace M] [SigmaCompactSpace M]
+  [TopologicalSpace M] [ChartedSpace H M]
   (IF : ModelWithCorners ℝ F H) [SmoothManifoldWithCorners IF M]
 
 /- Clearly should be generalised. Maybe what we really want is a theory of local diffeomorphisms.
@@ -286,6 +291,7 @@ theorem range_openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : PartialHomeomo
 
 variable {M} (F)
 variable [IF.Boundaryless] [FiniteDimensional ℝ F]
+variable [T2Space M] [LocallyCompactSpace M] [SigmaCompactSpace M]
 
 theorem nice_atlas' {ι : Type*} {s : ι → Set M} (s_op : ∀ j, IsOpen <| s j)
     (cov : (⋃ j, s j) = univ) (U : Set F) (hU₁ : (0 : F) ∈ U) (hU₂ : IsOpen U) :
@@ -369,14 +375,13 @@ variable {𝕜 EX EM EY EN EM' X M Y N M' : Type*} [NontriviallyNormedField 𝕜
   {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
   {HM' : Type*} [TopologicalSpace HM'] {IM' : ModelWithCorners 𝕜 EM' HM'}
   {HN : Type*} [TopologicalSpace HN] {IN : ModelWithCorners 𝕜 EN HN}
-  [TopologicalSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners IX X]
-  [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M]
+  [TopologicalSpace X] [ChartedSpace HX X]
+  [TopologicalSpace M] [ChartedSpace HM M]
   [TopologicalSpace M'] [ChartedSpace HM' M']
 
 section NonMetric
 
-variable [TopologicalSpace Y] [ChartedSpace HY Y] [SmoothManifoldWithCorners IY Y]
-  [TopologicalSpace N] [ChartedSpace HN N] [SmoothManifoldWithCorners IN N]
+variable [TopologicalSpace Y] [ChartedSpace HY Y] [TopologicalSpace N] [ChartedSpace HN N]
   (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (f : M → N) (g : X → Y)
 
 section
@@ -438,8 +443,8 @@ end NonMetric
 
 section Metric
 
-variable [MetricSpace Y] [ChartedSpace HY Y] [SmoothManifoldWithCorners IY Y] [MetricSpace N]
-  [ChartedSpace HN N] [SmoothManifoldWithCorners IN N] (φ : OpenSmoothEmbedding IX X IM M)
+variable [MetricSpace Y] [ChartedSpace HY Y] [MetricSpace N] [ChartedSpace HN N]
+  (φ : OpenSmoothEmbedding IX X IM M)
   (ψ : OpenSmoothEmbedding IY Y IN N) (f : M → N) (g : X → Y)
 
 /-- This is `lem:dist_updating` in the blueprint. -/

SphereEversion/Global/TwistOneJetSec.lean

@@ -21,7 +21,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCo
   [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners 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] (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V]
+  (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V]
   (V' : Type*) [NormedAddCommGroup V'] [NormedSpace 𝕜 V']
 
 section Smoothness
@@ -178,7 +178,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top
   [SmoothManifoldWithCorners I M] (V : Type*) [NormedAddCommGroup V] [NormedSpace ℝ V]
   (V' : Type*) [NormedAddCommGroup V'] [NormedSpace ℝ V'] {F : Type*} [NormedAddCommGroup F]
   [NormedSpace ℝ F] {G : Type*} [TopologicalSpace G] (J : ModelWithCorners ℝ F G) (N : Type*)
-  [TopologicalSpace N] [ChartedSpace G N] [SmoothManifoldWithCorners J N]
+  [TopologicalSpace N] [ChartedSpace G N]
 
 /-- A section of a 1-jet bundle seen as a bundle over the source manifold. -/
 @[ext]