chore: bump to v4.22.0 (#119)

Ruben-VandeVelde · web-flow · commit 2fa4816a19e3 · 2025-08-14T15:38:14.000+02:00
diff --git a/SphereEversion.lean b/SphereEversion.lean
@@ -34,7 +34,7 @@ import SphereEversion.ToMathlib.Analysis.Convex.Basic
 import SphereEversion.ToMathlib.Analysis.CutOff
 import SphereEversion.ToMathlib.Analysis.InnerProductSpace.CrossProduct
 import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Dual
-import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Projection
+import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Projection.Submodule
 import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Rotation
 import SphereEversion.ToMathlib.Analysis.Normed.Module.FiniteDimension
 import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc
diff --git a/SphereEversion/Global/LocalisationData.lean b/SphereEversion/Global/LocalisationData.lean
@@ -142,7 +142,7 @@ theorem localisation_stability {f : M → M'} (ld : LocalisationData I I' f) :
   refine ⟨δ ∘ f, fun m ↦ hδ₀ (f m), by fun_prop, fun g hg i ↦ ?_⟩
   rintro - ⟨e, rfl⟩
   have hi : f (ld.φ i e) ∈ K (ld.j i) :=
-    image_subset _ ball_subset_closedBall (ld.h₃ i (mem_range_self e))
+    image_mono ball_subset_closedBall (ld.h₃ i (mem_range_self e))
   exact hδ₁ (ld.j i) (f <| ld.φ i e) hi (le_of_lt (hg _))
 
 namespace LocalisationData
diff --git a/SphereEversion/Global/LocalizedConstruction.lean b/SphereEversion/Global/LocalizedConstruction.lean
@@ -105,6 +105,6 @@ theorem OpenSmoothEmbedding.improve_formalSol (φ : OpenSmoothEmbedding 𝓘(ℝ
       · have : ∀ᶠ x near φ '' K₀, x ∈ p.φ '' K₁ := by
           suffices ∀ᶠ x near φ '' K₀, x ∈ interior (p.φ '' K₁) from this.mono interior_subset
           exact isOpen_interior.mem_nhdsSet.mpr
-            ((image_subset φ hK₀K₁).trans (φ.isOpenMap.image_interior_subset K₁))
+            ((image_mono hK₀K₁).trans (φ.isOpenMap.image_interior_subset K₁))
         exact this.mono (fun a hx hx' ↦ (hx' hx).elim)
     · exact fun _ ↦ (p.mkHtpy_isHolonomicAt_iff hcompat).mpr
diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean
@@ -25,7 +25,7 @@ In this file we consider two manifolds `M` and `M'` with models `I` and `I'`
 
 noncomputable section
 
-open Set Function Filter ChartedSpace SmoothManifoldWithCorners
+open Set Function Filter ChartedSpace
 
 open scoped Topology Manifold ContDiff
 
diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean
@@ -7,7 +7,7 @@ open Set Function
 
 open Filter hiding map_smul
 
-open ChartedSpace SmoothManifoldWithCorners
+open ChartedSpace
 
 open LinearMap (ker)
 
diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean
@@ -23,7 +23,7 @@ open Set Function
 
 open Filter hiding map_smul
 
-open ChartedSpace SmoothManifoldWithCorners
+open ChartedSpace
 
 open scoped Topology Manifold Bundle ContDiff
 
diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean
@@ -369,7 +369,7 @@ theorem locFormalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) {x : E} (hx : smoot
   intro v
   have : (fun x : E ↦ ((1 : ℝ) - 2) • x) = fun x ↦ -x := by ext x; norm_num
   simp [this]
-  obtain ⟨v', hv', v, hv, rfl⟩ := Submodule.exists_add_mem_mem_orthogonal (ℝ ∙ x) v
+  obtain ⟨v', hv', v, hv, rfl⟩ := Submodule.exists_add_mem_mem_orthogonal (K := ℝ ∙ x) v
   simp_rw [ContinuousLinearMap.map_add, ω.rot_one _ hv, ω.rot_eq_of_mem_span (1, x) hv']
   rw [fderiv_fun_neg, fderiv_id']
   simp only [ContinuousLinearMap.neg_apply, ContinuousLinearMap.coe_id', id_eq, add_zero,
diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean
@@ -129,7 +129,7 @@ theorem ContDiff.periodize {f : ℝ → E} {n : ℕ∞} (h : ContDiff ℝ n f) (
     apply Nonempty.mono _ hi
     gcongr
     · rw [show (e i : ℝ → ℝ) = VAdd.vadd i by ext x; exact add_comm x i]
-      exact image_subset _ Ioo_subset_Icc_self
+      exact image_mono Ioo_subset_Icc_self
     exact subset_tsupport f
   · fun_prop
 
diff --git a/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean b/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean
@@ -90,7 +90,7 @@ theorem image_proj𝕊₁_Ico : proj𝕊₁ '' Ico 0 1 = univ := by
   exact fun x ↦ ⟨x.repr, x.repr_mem, x.proj_repr⟩
 
 theorem image_proj𝕊₁_Icc : proj𝕊₁ '' Icc 0 1 = univ :=
-  eq_univ_of_subset (image_subset proj𝕊₁ Ico_subset_Icc_self) image_proj𝕊₁_Ico
+  eq_univ_of_subset (image_mono Ico_subset_Icc_self) image_proj𝕊₁_Ico
 
 @[continuity, fun_prop]
 theorem continuous_proj𝕊₁ : Continuous proj𝕊₁ := continuous_quotient_mk'
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean
@@ -1,5 +1,5 @@
 import Mathlib.Analysis.InnerProductSpace.Dual
-import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Projection
+import SphereEversion.ToMathlib.Analysis.InnerProductSpace.Projection.Submodule
 
 open scoped RealInnerProductSpace
 
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection/Submodule.lean
@@ -1,4 +1,4 @@
-import Mathlib.Analysis.InnerProductSpace.Projection
+import Mathlib.Analysis.InnerProductSpace.Projection.Submodule
 
 noncomputable section
 
@@ -65,7 +65,7 @@ theorem orthogonal_line_inf {u v : E} : {.u}ᗮ ⊓ {.v}ᗮ = {.(pr[v]ᗮ u : E)
   rw [inf_orthogonal, inf_orthogonal]
   refine congr_arg _ (le_antisymm (sup_le ?_ le_sup_right) (sup_le ?_ le_sup_right)) <;>
     rw [span_singleton_le_iff_mem]
-  · nth_rw 2 [← starProjection_add_starProjection_orthogonal (Δ v) u]
+  · nth_rw 2 [← starProjection_add_starProjection_orthogonal (K := Δ v) u]
     exact add_mem (mem_sup_right <| coe_mem _) (mem_sup_left <| mem_span_singleton_self _)
   · rw [projSpanOrthogonal, orthogonalProjection_orthogonal]
     exact sub_mem (mem_sup_left <| mem_span_singleton_self _) (mem_sup_right <| coe_mem _)
@@ -112,7 +112,7 @@ theorem orthogonalProjection_orthogonal_singleton {x y : E} :
         rw [inner_sub_right, inner_smul_right]
         field_simp [inner_self_ne_zero.mpr hx]⟩ := by
   apply Subtype.ext
-  have := starProjection_add_starProjection_orthogonal (span ℝ ({x} : Set E)) y
+  have := starProjection_add_starProjection_orthogonal (K := span ℝ ({x} : Set E)) y
   simp [eq_sub_of_add_eq' this, starProjection_singleton, real_inner_self_eq_norm_sq]
 
 theorem coe_orthogonalProjection_orthogonal_singleton {x y : E} :
@@ -121,10 +121,10 @@ theorem coe_orthogonalProjection_orthogonal_singleton {x y : E} :
 
 theorem foo {x₀ x : E} (h : ⟪x₀, x⟫ ≠ 0) (y : E) (hy : y ∈ {.x₀}ᗮ) :
     (pr[x]ᗮ y : E) - (⟪x₀, pr[x]ᗮ y⟫ / ⟪x₀, x⟫) • x = y :=  by
-  conv_rhs => rw [← starProjection_add_starProjection_orthogonal (Δ x) y]
+  conv_rhs => rw [← starProjection_add_starProjection_orthogonal (K := Δ x) y]
   rw [starProjection_singleton, sub_eq_add_neg, add_comm, ← neg_smul]
   congr 2
-  have := starProjection_add_starProjection_orthogonal (Δ x) y
+  have := starProjection_add_starProjection_orthogonal (K := Δ x) y
   rw [starProjection_singleton] at this
   apply_fun fun z ↦ ⟪x₀, z⟫ at this
   rw [mem_orthogonal_span_singleton_iff.mp hy, inner_add_right, inner_smul_right] at this
diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean
@@ -48,7 +48,7 @@ def rotAux (p : ℝ × E) : E →L[ℝ] E :=
 theorem rot_eq_aux : ω.rot = ω.rotAux := by
   ext1 p
   dsimp [rot, rotAux]
-  rw [id_eq_sum_starProjection_self_orthogonalComplement (ℝ ∙ p.2)]
+  rw [id_eq_sum_starProjection_self_orthogonalComplement (K := ℝ ∙ p.2)]
   simp only [smul_add, sub_smul, one_smul, starProjection]
   abel
 
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -15,27 +15,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "968ea7f28314185cfc93c17b99f1c265af095b1b",
+   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c37191eba2da78393070da8c4367689d8c4276e4",
+   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,50 +45,50 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4241928fd3ebae83a037a253e39d9b773e34c3b4",
+   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e",
+   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.67",
+   "inputRev": "v0.0.68",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc",
+   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef3dac0f872ca6aaa7d02e015427e06dd0b6195",
+   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6a49e4c22164b1d18665837cf1e148131c7a6c4d",
+   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.22.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc4
+leanprover/lean4:v4.22.0
