From f94a86de9f712fc2a62d8d1244b303b73cd99834 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Wed, 20 Nov 2024 15:35:14 +0100
Subject: [PATCH] chore: fix some more variable inclusion/omission warnings

---
 SphereEversion/Global/Immersion.lean            |  3 +++
 SphereEversion/Global/Localisation.lean         |  3 +++
 SphereEversion/Global/OneJetBundle.lean         | 15 +++++++++++++++
 SphereEversion/Global/ParametricityForFree.lean | 14 ++++++--------
 SphereEversion/Global/Relation.lean             |  9 ++++++++-
 5 files changed, 35 insertions(+), 9 deletions(-)

diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean
index c169ad0d..e1e232e8 100644
--- a/SphereEversion/Global/Immersion.lean
+++ b/SphereEversion/Global/Immersion.lean
@@ -35,6 +35,7 @@ variable (M M') in
 def immersionRel : RelMfld I M I' M' :=
   {σ | Injective σ.2}
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners 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' _) :=
@@ -64,6 +65,7 @@ theorem immersionRel_open [FiniteDimensional ℝ E] : IsOpen (immersionRel I M I
   · infer_instance
   · infer_instance
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners 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 φ) :
@@ -72,6 +74,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
 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))
diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean
index 44ea2b9d..f1cd1dbc 100644
--- a/SphereEversion/Global/Localisation.lean
+++ b/SphereEversion/Global/Localisation.lean
@@ -145,6 +145,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
 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
@@ -154,6 +155,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
 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
@@ -164,6 +166,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
 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
diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean
index 1a816c64..5eaae7a5 100644
--- a/SphereEversion/Global/OneJetBundle.lean
+++ b/SphereEversion/Global/OneJetBundle.lean
@@ -130,6 +130,7 @@ variable {I I' M M'}
 
 @[inherit_doc] local notation "HJ" => ModelProd (ModelProd H H') (E →L[𝕜] E')
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 @[ext]
 theorem OneJetBundle.ext {x y : J¹MM'} (h : x.1.1 = y.1.1) (h' : x.1.2 = y.1.2) (h'' : x.2 = y.2) :
     x = y := by
@@ -339,11 +340,13 @@ theorem SmoothAt.oneJetBundle_proj {f : N → J¹MM'} {x₀ : N}
 def OneJetBundle.mk (x : M) (y : M') (f : OneJetSpace I I' (x, y)) : J¹MM' :=
   ⟨(x, y), f⟩
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 @[simp, mfld_simps]
 theorem oneJetBundle_mk_fst {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} :
     (OneJetBundle.mk x y f).1 = (x, y) :=
   rfl
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 @[simp, mfld_simps]
 theorem oneJetBundle_mk_snd {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} :
     (OneJetBundle.mk x y f).2 = f :=
@@ -469,6 +472,9 @@ protected def OneJetBundle.map (f : M → N) (g : M' → N')
 
 variable {I' J'}
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
+  [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃]
+  [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in
 theorem OneJetBundle.map_map {f₂ : N → M₂} {f : M → N} {g₂ : N' → M₃} {g : M' → N'}
     {Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x}
     {Df₂inv : ∀ x : N, TangentSpace I₂ (f₂ x) →L[𝕜] TangentSpace J x} {x : J¹MM'}
@@ -481,6 +487,9 @@ theorem OneJetBundle.map_map {f₂ : N → M₂} {f : M → N} {g₂ : N' → M
   · dsimp only [OneJetBundle.map, OneJetBundle.mk]
     simp_rw [← ContinuousLinearMap.comp_assoc, mfderiv_comp x.1.2 hg₂ hg]
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
+  [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃]
+  [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in
 theorem OneJetBundle.map_id (x : J¹MM') :
     OneJetBundle.map I' I' id id (fun x ↦ ContinuousLinearMap.id 𝕜 (TangentSpace I x)) x = x := by
   -- Porting note: was `ext _` in Lean 3
@@ -516,6 +525,9 @@ theorem SmoothAt.oneJetBundle_map {f : M'' → M → N} {g : M'' → M' → N'}
 def mapLeft (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) :
     J¹MM' → OneJetBundle J N I' M' := fun p ↦ OneJetBundle.mk (f p.1.1) p.1.2 (p.2 ∘L Dfinv p.1.1)
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
+  [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃]
+  [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in
 theorem mapLeft_eq_map (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) :
     mapLeft f Dfinv = OneJetBundle.map I' I' f (id : M' → M') Dfinv := by
   ext x; rfl; rfl; dsimp only [OneJetBundle.map, mapLeft, oneJetBundle_mk_snd]
@@ -541,6 +553,9 @@ def bundleFst : OneJetBundle (J.prod I) (N × M) I' M' → OneJetBundle J N I' M
 def bundleSnd : OneJetBundle (J.prod I) (N × M) I' M' → J¹MM' :=
   mapLeft Prod.snd fun x ↦ mfderiv I (J.prod I) (fun y ↦ (x.1, y)) x.2
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
+  [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃]
+  [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in
 theorem bundleSnd_eq (x : OneJetBundle (J.prod I) (N × M) I' M') :
     bundleSnd x = (mapLeft Prod.snd (fun _ ↦ ContinuousLinearMap.inr 𝕜 F E) x : J¹MM') := by
   simp_rw [bundleSnd, mfderiv_prod_right]; rfl
diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean
index c587f04a..c9a118ed 100644
--- a/SphereEversion/Global/ParametricityForFree.lean
+++ b/SphereEversion/Global/ParametricityForFree.lean
@@ -35,14 +35,12 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top
 
 variable {R : RelMfld I M I' M'}
 
-variable (IP P)
-
+variable (IP P) in
 /-- The relation `𝓡 ^ P` -/
 def RelMfld.relativize (R : RelMfld I M I' M') : RelMfld (IP.prod I) (P × M) I' M' :=
   bundleSnd ⁻¹' R
 
-variable {IP P}
-
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners IP P] in
 theorem RelMfld.mem_relativize (R : RelMfld I M I' M')
     (w : OneJetBundle (IP.prod I) (P × M) I' M') :
     w ∈ R.relativize IP P ↔
@@ -66,6 +64,7 @@ variable {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
 #check (R.relativize IP P).slice σ p
 #check (R.slice (bundleSnd σ) q : Set <| TangentSpace I' σ.proj.2) -/
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners IP P] in
 theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
     {p : DualPair <| TangentSpace (IP.prod I) σ.1.1} (q : DualPair <| TangentSpace I σ.1.1.2)
     (hpq : p.π.comp (ContinuousLinearMap.inr ℝ EP E) = q.π) :
@@ -94,6 +93,7 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
   erw [← preimage_vadd_neg, mem_preimage, mem_slice, R.mem_relativize]
   congr!
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners IP P] in
 theorem relativize_slice_eq_univ {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
     {p : DualPair <| TangentSpace (IP.prod I) σ.1.1}
     (hp : p.π.comp (ContinuousLinearMap.inr ℝ EP E) = 0) :
@@ -119,8 +119,8 @@ theorem relativize_slice_eq_univ {σ : OneJetBundle (IP.prod I) (P × M) I' M'}
   dsimp only [oneJetBundle_mk_fst, oneJetBundle_mk_snd]
   simp [this, exists_const, forall_const]
 
-variable (IP P)
-
+variable (IP P) in
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners IP P] in
 theorem RelMfld.Ample.relativize (hR : R.Ample) : (R.relativize IP P).Ample := by
   intro σ p
   let p2 := p.π.comp (ContinuousLinearMap.inr ℝ EP E)
@@ -135,8 +135,6 @@ theorem RelMfld.Ample.relativize (hR : R.Ample) : (R.relativize IP P).Ample := b
   rw [relativize_slice q rfl]
   exact (hR q).vadd
 
-variable {IP P}
-
 theorem FamilyOneJetSec.uncurry_mem_relativize (S : FamilyOneJetSec I M I' M' IP P) {s : P}
     {x : M} : S.uncurry (s, x) ∈ R.relativize IP P ↔ S s x ∈ R := by
   simp_rw [RelMfld.relativize, mem_preimage, bundleSnd_eq, OneJetSec.coe_apply, mapLeft]
diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean
index 43baaa22..644af0a4 100644
--- a/SphereEversion/Global/Relation.lean
+++ b/SphereEversion/Global/Relation.lean
@@ -176,13 +176,14 @@ def RelMfld.slice (R : RelMfld I M I' M') (σ : OneJetBundle I M I' M') (p : Dua
     Set (TM' σ.1.2) :=
   {w : TM' σ.1.2 | OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R}
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 /-- For some reason `rw [mem_setOf_eq]` fails after unfolding `slice`,
 but rewriting with this lemma works. -/
 theorem mem_slice {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : DualPair <| TM σ.1.1}
     {w : TM' σ.1.2} : w ∈ R.slice σ p ↔ OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R :=
   Iff.rfl
 
-
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'}
     {p : DualPair <| TM σ.1.1} (x : E') :
     R.slice (OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 x)) p = (R.slice σ p : Set E') := by
@@ -196,6 +197,7 @@ theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'}
 def RelMfld.Ample (R : RelMfld I M I' M') : Prop :=
   ∀ ⦃σ : OneJetBundle I M I' M'⦄ (p : DualPair <| TM σ.1.1), AmpleSet (R.slice σ p)
 
+omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 theorem RelMfld.ample_iff (R : RelMfld I M I' M') :
     R.Ample ↔
       ∀ ⦃σ : OneJetBundle I M I' M'⦄ (p : DualPair <| TM σ.1.1), σ ∈ R → AmpleSet (R.slice σ p) := by
@@ -483,6 +485,8 @@ theorem OpenSmoothEmbedding.smooth_transfer :
 theorem OneJetBundle.continuous_transfer : Continuous (φ.transfer ψ) :=
   (OpenSmoothEmbedding.smooth_transfer _ _).continuous
 
+omit [SmoothManifoldWithCorners IX X] [SmoothManifoldWithCorners IM M]
+  [SmoothManifoldWithCorners IY Y] [SmoothManifoldWithCorners IN N] in
 theorem OpenSmoothEmbedding.range_transfer :
     range (φ.transfer ψ) = π _ (OneJetSpace IM IN) ⁻¹' range φ ×ˢ range ψ := by
   ext σ; constructor
@@ -502,6 +506,7 @@ theorem OpenSmoothEmbedding.range_transfer :
     erw [(φ.fderiv x).apply_symm_apply]
     rfl
 
+omit [SmoothManifoldWithCorners IX X] [SmoothManifoldWithCorners IY Y] in
 theorem OpenSmoothEmbedding.isOpen_range_transfer : IsOpen (range (φ.transfer ψ)) := by
   rw [φ.range_transfer ψ]
   exact (φ.isOpen_range.prod ψ.isOpen_range).preimage oneJetBundle_proj_continuous
@@ -517,6 +522,8 @@ instance (y : Y) : NormedAddCommGroup (TY y) := by assumption
 
 instance (y : Y) : NormedSpace ℝ (TY y) := by assumption
 
+omit [SmoothManifoldWithCorners IX X] [SmoothManifoldWithCorners IM M]
+  [SmoothManifoldWithCorners IY Y] [SmoothManifoldWithCorners IN N] in
 /-- Ampleness survives localization -/
 theorem RelMfld.Ample.localize (hR : R.Ample) : (R.localize φ ψ).Ample := by
   intro x p