diff --git a/MIL/C08_Groups_and_Rings/S02_Rings.lean b/MIL/C08_Groups_and_Rings/S02_Rings.lean
index b18442e6..8c5c021d 100644
--- a/MIL/C08_Groups_and_Rings/S02_Rings.lean
+++ b/MIL/C08_Groups_and_Rings/S02_Rings.lean
@@ -1,5 +1,5 @@
 -- BOTH:
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Localization.Basic
 import Mathlib.RingTheory.DedekindDomain.Ideal
 import Mathlib.Analysis.Complex.Polynomial.Basic
@@ -560,9 +560,9 @@ since it does not assume the existence of a ``Algebra R S`` instance, so dot not
 you would expect.
 EXAMPLES: -/
 -- QUOTE:
-#check (Complex.ofReal : ℝ →+* ℂ)
+#check (Complex.ofRealHom : ℝ →+* ℂ)
 
-example : (X ^ 2 + 1 : ℝ[X]).eval₂ Complex.ofReal Complex.I = 0 := by simp
+example : (X ^ 2 + 1 : ℝ[X]).eval₂ Complex.ofRealHom Complex.I = 0 := by simp
 -- QUOTE.
 
 /- TEXT:
diff --git a/MIL/C09_Linear_Algebra/S02_Subspaces.lean b/MIL/C09_Linear_Algebra/S02_Subspaces.lean
index f77565cf..b03b7c7f 100644
--- a/MIL/C09_Linear_Algebra/S02_Subspaces.lean
+++ b/MIL/C09_Linear_Algebra/S02_Subspaces.lean
@@ -246,8 +246,7 @@ example : GaloisInsertion (Submodule.span K) ((↑) : Submodule K V → Set V) :
 When those are not enough, one can use the relevant induction principle
 ``Submodule.span_induction`` which ensures a property holds for every element of the
 span of ``s`` as long as it holds on ``zero`` and elements of ``s`` and is stable under
-sum and scalar multiplication. As usual with such lemmas, Lean sometimes needs help
-to figure out the predicate we are interested in.
+sum and scalar multiplication.
 
 As an exercise, let us reprove one implication of ``Submodule.mem_sup``.
 Remember that you can use the `module` tactic to close goals that follow from
@@ -258,26 +257,35 @@ EXAMPLES: -/
 example {S T : Submodule K V} {x : V} (h : x ∈ S ⊔ T) :
     ∃ s ∈ S, ∃ t ∈ T, x = s + t  := by
   rw [← S.span_eq, ← T.span_eq, ← Submodule.span_union] at h
-  apply Submodule.span_induction h (p := fun x ↦ ∃ s ∈ S, ∃ t ∈ T, x = s + t)
+  induction h using Submodule.span_induction with
 /- EXAMPLES:
-  · sorry
-  · sorry
-  · sorry
-  · sorry
+  | mem y h =>
+      sorry
+  | zero =>
+      sorry
+  | add x y hx hy hx' hy' =>
+      sorry
+  | smul a x hx hx' =>
+      sorry
 SOLUTIONS: -/
-  · rintro x (hx|hx)
-    · use x, hx, 0, T.zero_mem
+  | mem x h =>
+      rcases h with (hx|hx)
+      · use x, hx, 0, T.zero_mem
+        module
+      · use 0, S.zero_mem, x, hx
+        module
+  | zero =>
+      use 0, S.zero_mem, 0, T.zero_mem
       module
-    · use 0, S.zero_mem, x, hx
+  | add x y hx hy hx' hy' =>
+      rcases hx' with ⟨s, hs, t, ht, rfl⟩
+      rcases hy' with ⟨s', hs', t', ht', rfl⟩
+      use s + s', S.add_mem hs hs', t + t', T.add_mem ht ht'
+      module
+  | smul a x hx hx' =>
+      rcases hx' with ⟨s, hs, t, ht, rfl⟩
+      use a • s, S.smul_mem a hs, a • t, T.smul_mem a ht
       module
-  · use 0, S.zero_mem, 0, T.zero_mem
-    module
-  · rintro - - ⟨s, hs, t, ht, rfl⟩ ⟨s', hs', t', ht', rfl⟩
-    use s + s', S.add_mem hs hs', t + t', T.add_mem ht ht'
-    module
-  · rintro a - ⟨s, hs, t, ht, rfl⟩
-    use a • s, S.smul_mem a hs, a • t, T.smul_mem a ht
-    module
 
 -- QUOTE.
 /- TEXT:
diff --git a/MIL/C09_Linear_Algebra/S03_Endomorphisms.lean b/MIL/C09_Linear_Algebra/S03_Endomorphisms.lean
index 639d6c40..766f11ff 100644
--- a/MIL/C09_Linear_Algebra/S03_Endomorphisms.lean
+++ b/MIL/C09_Linear_Algebra/S03_Endomorphisms.lean
@@ -98,27 +98,16 @@ SOLUTIONS: -/
 
 -- QUOTE.
 /- TEXT:
-We now move to the discussions of eigenspaces and eigenvalues. By the definition, the eigenspace
+We now move to the discussions of eigenspaces and eigenvalues. The eigenspace
 associated to an endomorphism :math:`φ` and a scalar :math:`a` is the kernel of :math:`φ - aId`.
-The first thing to understand is how to spell :math:`aId`. We could use
-``a • LinearMap.id``, but Mathlib uses `algebraMap K (End K V) a` which directly plays nicely
-with the ``K``-algebra structure.
-
-EXAMPLES: -/
--- QUOTE:
-example (a : K) : algebraMap K (End K V) a = a • LinearMap.id := rfl
-
--- QUOTE.
-/- TEXT:
-Then the next thing to note is that eigenspaces are defined for all values of ``a``, although
+Eigenspaces are defined for all values of ``a``, although
 they are interesting only when they are non-zero.
 However an eigenvector is, by definition, a non-zero element of an eigenspace. The corresponding
 predicate is ``End.HasEigenvector``.
 EXAMPLES: -/
 -- QUOTE:
-example (φ : End K V) (a : K) :
-    φ.eigenspace a = LinearMap.ker (φ - algebraMap K (End K V) a) :=
-  rfl
+example (φ : End K V) (a : K) : φ.eigenspace a = LinearMap.ker (φ - a • 1) :=
+  End.eigenspace_def
 
 
 -- QUOTE.
diff --git a/MIL/C10_Topology/S01_Filters.lean b/MIL/C10_Topology/S01_Filters.lean
index 38ec6bbb..4f6750ee 100644
--- a/MIL/C10_Topology/S01_Filters.lean
+++ b/MIL/C10_Topology/S01_Filters.lean
@@ -298,7 +298,7 @@ example (f : ℕ → ℝ × ℝ) (x₀ y₀ : ℝ) :
       Tendsto (Prod.fst ∘ f) atTop (𝓝 x₀) ∧ Tendsto (Prod.snd ∘ f) atTop (𝓝 y₀) := by
   rw [nhds_prod_eq]
   unfold Tendsto SProd.sprod Filter.instSProd Filter.prod
-  erw [le_inf_iff, ← map_le_iff_le_comap, map_map, ← map_le_iff_le_comap, map_map]
+  rw [le_inf_iff, ← map_le_iff_le_comap, map_map, ← map_le_iff_le_comap, map_map]
 
 /- TEXT:
 The ordered type ``Filter X`` is actually a *complete* lattice,
diff --git a/lake-manifest.json b/lake-manifest.json
index 53509916..88a06d01 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "13f9b00769bdac2c0041406a6c2524a361e8d660",
+   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
+   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,16 +35,16 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "rev": "23268f52d3505955de3c26a42032702c25cfcbf8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
+   "inputRev": "v0.0.44",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
+   "scope": "leanprover",
    "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "63a7d4a353f48f6c5f1bc19d0f018b0513cb370a",
+   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,20 +65,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "781beceb959c68b36d3d96205b3531e341879d2c",
+   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d212dd74414e997653cd3484921f4159c955ccca",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5e050d47562fa4938a5f9afbc006c7f02f4544aa",
+   "rev": "d7317655e2826dc1f1de9a0c138db2775c4bb841",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.13.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mil",
diff --git a/lakefile.lean b/lakefile.lean
index e658efe6..0666a963 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -10,5 +10,5 @@ package mil where
 @[default_target]
 lean_lib MIL where
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"
+require mathlib from git "https://github.com/leanprover-community/mathlib4"@"v4.13.0"
 
diff --git a/lean-toolchain b/lean-toolchain
index eff86fd6..4f86f953 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc3
+leanprover/lean4:v4.13.0