From 515f02f28a316240187594a82b1882e21a7efbf6 Mon Sep 17 00:00:00 2001
From: "Gregory C. Wickham" <10427906+gw90@users.noreply.github.com>
Date: Sun, 10 May 2026 18:21:38 +0000
Subject: [PATCH 01/11] feat(Analysis/CStarAlgebra/Spectrum): Adding lemmas
 that the CStarAlgebra norm equals the square root of the spectral radius of
 star a * a (#33178)

Adds lemmas that the ||a||^2_A=sqrt(spectralRadius C (star a * a)). I think it would be helpful to have these lemmas available in Mathlib. It'll help with some of the other things I'm working on. Feel free to move them to a different file or rename them as you see fit.

Co-authored-by: Gregory Wickham <gwickham99@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
---
 Mathlib/Analysis/CStarAlgebra/Spectrum.lean | 23 +++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean
index 2f7e5a5c63..adf1bd2602 100644
--- a/Mathlib/Analysis/CStarAlgebra/Spectrum.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Spectrum.lean
@@ -42,6 +42,8 @@ we can still establish a form of spectral permanence.
   to its norm.
 + `IsStarNormal.spectralRadius_eq_nnnorm`: The spectral radius of a normal element is equal to
   its norm.
++ `spectralRadius_toReal_star_self_mul_self_eq_normSq`: The spectral radius of `a⋆ * a` is equal to
+  the square of the norm of `a`.
 + `IsSelfAdjoint.mem_spectrum_eq_re`: Any element of the spectrum of a selfadjoint element is real.
 * `StarSubalgebra.coe_isUnit`: for `x : S` in a C⋆-Subalgebra `S` of `A`, then `↑x : A` is a Unit
   if and only if `x` is a unit.
@@ -149,6 +151,27 @@ theorem IsStarNormal.spectralRadius_eq_nnnorm (a : A) [IsStarNormal a] :
   convert tendsto_nhds_unique h₂ (pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a⋆ * a))
   rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_mul]
 
+namespace CStarAlgebra
+
+theorem toReal_spectralRadius_star_mul_self_eq_norm_sq (a : A) :
+    (spectralRadius ℂ (a⋆ * a)).toReal = ‖a‖ ^ 2 := by
+  rw [(IsSelfAdjoint.star_mul_self a).toReal_spectralRadius_complex_eq_norm,
+    CStarRing.norm_star_mul_self, ← pow_two]
+
+theorem toReal_spectralRadius_self_mul_star_eq_norm_sq (a : A) :
+    (spectralRadius ℂ (a * a⋆)).toReal = ‖a‖ ^ 2 := by
+  rw [← norm_star a, ← toReal_spectralRadius_star_mul_self_eq_norm_sq, star_star]
+
+theorem sqrt_toReal_spectralRadius_star_mul_self_eq_norm (a : A) :
+    (spectralRadius ℂ (a⋆ * a)).toReal.sqrt = ‖a‖ := by
+  simp [toReal_spectralRadius_star_mul_self_eq_norm_sq]
+
+theorem sqrt_toReal_spectralRadius_self_mul_star_eq_norm (a : A) :
+    (spectralRadius ℂ (a * a⋆)).toReal.sqrt = ‖a‖ := by
+  simp [toReal_spectralRadius_self_mul_star_eq_norm_sq]
+
+end CStarAlgebra
+
 variable [StarModule ℂ A]
 
 /-- Any element of the spectrum of a selfadjoint is real. -/

From 0346a02b8f903db8c3d292a7fa4e67d935632c9d Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <5110976+kebekus@users.noreply.github.com>
Date: Sun, 10 May 2026 18:21:40 +0000
Subject: [PATCH 02/11] feat: integrability of terms in Cartan's formula
 (#38581)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

If `f : ℂ → ℂ` is meromorphic, establish the circle integrability of the function `a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` and compute values of the circle integral. The circle integral in question is one of the main terms in Cartan's classic formula, describing the characteristic function `characteristic f ⊤ r` as a sum of circle averages.

This is the second section of a four-part PR, establishing Cartan's formula and its most immediate corollaries.
---
 Mathlib.lean                                  |   1 +
 .../Complex/ValueDistribution/Cartan.lean     | 139 +++++++++++++++++
 Mathlib/Analysis/Meromorphic/Basic.lean       |  32 ++++
 Mathlib/Analysis/Meromorphic/Order.lean       |  19 +++
 .../Meromorphic/TrailingCoefficient.lean      | 147 +++++++++++++++++-
 Mathlib/Topology/DiscreteSubset.lean          |  24 +++
 6 files changed, 361 insertions(+), 1 deletion(-)
 create mode 100644 Mathlib/Analysis/Complex/ValueDistribution/Cartan.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index eaa7c935f1..aa639e5979 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1867,6 +1867,7 @@ public import Mathlib.Analysis.Complex.UpperHalfPlane.Metric
 public import Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
 public import Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
 public import Mathlib.Analysis.Complex.UpperHalfPlane.Topology
+public import Mathlib.Analysis.Complex.ValueDistribution.Cartan
 public import Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
 public import Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
 public import Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
diff --git a/Mathlib/Analysis/Complex/ValueDistribution/Cartan.lean b/Mathlib/Analysis/Complex/ValueDistribution/Cartan.lean
new file mode 100644
index 0000000000..06ec0547d4
--- /dev/null
+++ b/Mathlib/Analysis/Complex/ValueDistribution/Cartan.lean
@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2026 Stefan Kebekus. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matteo Cipollina, Stefan Kebekus
+-/
+
+module
+
+public import Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
+
+/-!
+# Cartan's Formula
+
+This file will, in the future, establish Cartan's classic formula, describing the characteristic
+function `characteristic f ⊤ r` as a sum of two circle averages,
+
+- `circleAverage (logCounting f · r) 0 1` and
+- `circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖) 0 1`.
+
+As a corollary, Cartan's formula implies the (surprising, non-trival) fact that the characteristic
+function is monotone.
+
+At present, this file establishes circle integrability of the function
+`a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` and computes values of the circle integral.
+
+## References
+
+See Section VI.2 of [Lang, *Introduction to Complex Hyperbolic Spaces*][MR886677] for a detailed
+discussion.
+
+
+## TODO
+
+- Establish Cartan's Formula in full
+- Prove monotonicity of the characteristic function
+-/
+
+public section
+
+open Filter Metric Real Set Topology
+
+variable {f : ℂ → ℂ}
+
+namespace ValueDistribution
+
+/-!
+## Terms in Cartan's formula
+-/
+
+private lemma log_trailingCoeff_eq_zero_on_unitSphere {a : ℂ} (h : 0 < meromorphicOrderAt f 0)
+    (ha : a ∈ sphere 0 |1|) :
+    log ‖meromorphicTrailingCoeffAt (f · - a) 0‖ = 0 := by
+  simp_rw [sub_eq_neg_add]
+  rw [(meromorphicAt_of_meromorphicOrderAt_ne_zero
+    h.ne').meromorphicTrailingCoeffAt_fun_add_eq_left_of_lt]
+  · aesop
+  · rw [meromorphicOrderAt_const]
+    aesop
+
+private lemma eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero (h₁ : MeromorphicAt f 0)
+    (h₂ : meromorphicOrderAt f 0 = 0) :
+    (log ‖meromorphicTrailingCoeffAt f 0 - ·‖) =ᶠ[codiscreteWithin (sphere 0 |1|)]
+      fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖ := by
+  filter_upwards [self_mem_codiscreteWithin (sphere 0 |1|), compl_singleton_mem_codiscreteWithin
+    (meromorphicTrailingCoeffAt f 0)] with a ha_sphere ha_ne
+  congr
+  rw [h₁.meromorphicTrailingCoeffAt_fun_sub_eq_sub
+    (by fun_prop), meromorphicTrailingCoeffAt_const, sub_eq_add_neg]
+  · simp only [meromorphicOrderAt_const]
+    aesop
+  · simp only [meromorphicTrailingCoeffAt_const, ne_eq]
+    grind
+
+/--
+Circle integrability of the term `fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` that
+appears in Cartan's formula.
+-/
+theorem circleIntegrable_log_meromorphicTrailingCoeffAt :
+    CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖) 0 1 := by
+  by_cases h: ¬MeromorphicAt f 0
+  · have {a : ℂ} : ¬MeromorphicAt (fun x ↦ f x - a) 0 := by
+      rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]
+    simp_all
+  rcases lt_trichotomy (meromorphicOrderAt f 0) 0 with hneg | hzero | hpos
+  · refine (circleIntegrable_congr fun a ha ↦ ?_).2 (circleIntegrable_const
+      (log ‖meromorphicTrailingCoeffAt f 0‖) 0 1)
+    rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]
+    rw [meromorphicOrderAt_const]
+    aesop
+  · apply CircleIntegrable.congr_codiscreteWithin
+     (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero (not_not.1 h) hzero)
+    simpa [norm_sub_rev] using circleIntegrable_log_norm_sub_const 1
+  · apply (circleIntegrable_congr _).2 (circleIntegrable_const 0 0 1)
+    exact fun _ ↦ log_trailingCoeff_eq_zero_on_unitSphere hpos
+
+/--
+Circle average of the function `fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` that appears
+in Cartan's formula, in case where `f` has a zero at the origin.
+-/
+theorem circleAverage_log_norm_meromorphicTrailingCoeffAt_of_meromorphicOrderAt_pos
+    (h : 0 < meromorphicOrderAt f 0) :
+    circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖) 0 1 = 0 :=
+  circleAverage_const_on_circle (fun _ hx ↦ log_trailingCoeff_eq_zero_on_unitSphere h hx)
+
+/--
+Circle average of the function `fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` that appears
+in Cartan's formula, in case where  `f` has order zero at the origin.
+-/
+theorem circleAverage_log_norm_meromorphicTrailingCoeffAt_of_meromorphicOrderAt_eq_zero
+    (h : meromorphicOrderAt f 0 = 0) :
+    circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖) 0 1
+      = log⁺ ‖meromorphicTrailingCoeffAt f 0‖ := by
+  by_cases hf : MeromorphicAt f 0
+  · rw [← circleAverage_congr_codiscreteWithin
+      (eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero hf h) zero_ne_one.symm]
+    simp_rw [norm_sub_rev]
+    rw [circleAverage_log_norm_sub_const_eq_posLog]
+  have {a : ℂ} : ¬ MeromorphicAt (fun x ↦ f x - a) 0 := by
+    rwa [MeromorphicAt.meromorphicAt_fun_sub_iff_meromorphicAt₂ (by fun_prop)]
+  simp_all [circleAverage_const]
+
+/--
+Circle average of the function `fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖` that appears
+in Cartan's formula, in case where `f` has a pole at the origin.
+-/
+theorem circleAverage_log_norm_meromorphicTrailingCoeffAt_of_meromorphicOrderAt_lt_zero
+    (h : meromorphicOrderAt f 0 < 0) :
+    circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (f · - a) 0‖) 0 1
+      = log ‖meromorphicTrailingCoeffAt f 0‖ := by
+  rw [circleAverage_congr_sphere (f₂ := fun _ ↦ log ‖meromorphicTrailingCoeffAt f 0‖),
+    circleAverage_const]
+  intro a ha
+  simp only
+  congr 2
+  rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]
+  rw [meromorphicOrderAt_const]
+  aesop
+
+end ValueDistribution
diff --git a/Mathlib/Analysis/Meromorphic/Basic.lean b/Mathlib/Analysis/Meromorphic/Basic.lean
index 6d1087d688..49c044035d 100644
--- a/Mathlib/Analysis/Meromorphic/Basic.lean
+++ b/Mathlib/Analysis/Meromorphic/Basic.lean
@@ -188,6 +188,14 @@ lemma meromorphicAt_add_iff_meromorphicAt₁ {f g : 𝕜 → E} (hf : Meromorphi
     MeromorphicAt (f + g) x ↔ MeromorphicAt g x := by
   exact ⟨fun h ↦ by simpa using h.sub hf, fun _ ↦ by fun_prop⟩
 
+/--
+If `f` is meromorphic at `x`, then `f + g` is meromorphic at `x` if and only if `g` is meromorphic
+at `x`.
+-/
+lemma meromorphicAt_fun_add_iff_meromorphicAt₁ {f g : 𝕜 → E} (hf : MeromorphicAt f x) :
+    MeromorphicAt (fun z ↦ f z + g z) x ↔ MeromorphicAt g x :=
+  meromorphicAt_add_iff_meromorphicAt₁ hf
+
 /--
 If `g` is meromorphic at `x`, then `f + g` is meromorphic at `x` if and only if `f` is meromorphic
 at `x`.
@@ -197,6 +205,14 @@ lemma meromorphicAt_add_iff_meromorphicAt₂ {f g : 𝕜 → E} (hg : Meromorphi
   rw [add_comm]
   exact meromorphicAt_add_iff_meromorphicAt₁ hg
 
+/--
+If `g` is meromorphic at `x`, then `f + g` is meromorphic at `x` if and only if `f` is meromorphic
+at `x`.
+-/
+lemma meromorphicAt_fun_add_iff_meromorphicAt₂ {f g : 𝕜 → E} (hg : MeromorphicAt g x) :
+    MeromorphicAt (fun z ↦ f z + g z) x ↔ MeromorphicAt f x :=
+  meromorphicAt_add_iff_meromorphicAt₂ hg
+
 /--
 If `f` is meromorphic at `x`, then `f - g` is meromorphic at `x` if and only if `g` is meromorphic
 at `x`.
@@ -205,6 +221,14 @@ lemma meromorphicAt_sub_iff_meromorphicAt₁ {f g : 𝕜 → E} (hf : Meromorphi
     MeromorphicAt (f - g) x ↔ MeromorphicAt g x := by
   exact ⟨fun h ↦ by simpa using h.sub hf, fun _ ↦ by fun_prop⟩
 
+/--
+If `f` is meromorphic at `x`, then `f - g` is meromorphic at `x` if and only if `g` is meromorphic
+at `x`.
+-/
+lemma meromorphicAt_fun_sub_iff_meromorphicAt₁ {f g : 𝕜 → E} (hf : MeromorphicAt f x) :
+    MeromorphicAt (fun z ↦ f z - g z) x ↔ MeromorphicAt g x :=
+  meromorphicAt_sub_iff_meromorphicAt₁ hf
+
 /--
 If `g` is meromorphic at `x`, then `f - g` is meromorphic at `x` if and only if `f` is meromorphic
 at `x`.
@@ -213,6 +237,14 @@ lemma meromorphicAt_sub_iff_meromorphicAt₂ {f g : 𝕜 → E} (hg : Meromorphi
     MeromorphicAt (f - g) x ↔ MeromorphicAt f x := by
   exact ⟨fun h ↦ by simpa using h.add hg, fun _ ↦ by fun_prop⟩
 
+/--
+If `g` is meromorphic at `x`, then `f - g` is meromorphic at `x` if and only if `f` is meromorphic
+at `x`.
+-/
+lemma meromorphicAt_fun_sub_iff_meromorphicAt₂ {f g : 𝕜 → E} (hg : MeromorphicAt g x) :
+    MeromorphicAt (fun z ↦ f z - g z) x ↔ MeromorphicAt f x :=
+  meromorphicAt_sub_iff_meromorphicAt₂ hg
+
 /-- With our definitions, `MeromorphicAt f x` depends only on the values of `f` on a punctured
 neighbourhood of `x` (not on `f x`) -/
 lemma congr {f g : 𝕜 → E} (hf : MeromorphicAt f x) (hfg : f =ᶠ[𝓝[≠] x] g) :
diff --git a/Mathlib/Analysis/Meromorphic/Order.lean b/Mathlib/Analysis/Meromorphic/Order.lean
index 327418436d..6fe62f5a95 100644
--- a/Mathlib/Analysis/Meromorphic/Order.lean
+++ b/Mathlib/Analysis/Meromorphic/Order.lean
@@ -384,6 +384,25 @@ The order of a constant function is `⊤` if the constant is zero and `0` otherw
 We establish additivity of the order under multiplication and taking powers.
 -/
 
+/-- The order of a function `f` equals the order of `-f`. -/
+theorem meromorphicOrderAt_neg {f : 𝕜 → E} :
+    meromorphicOrderAt f x = meromorphicOrderAt (-f) x := by
+  by_cases h₁ : ¬MeromorphicAt f x
+  · aesop
+  rw [not_not] at h₁
+  by_cases h₂ : meromorphicOrderAt f x = ⊤
+  · rw [h₂, eq_comm]
+    simp_all [meromorphicOrderAt_eq_top_iff]
+  lift meromorphicOrderAt f x to ℤ using h₂ with n hn
+  rw [eq_comm, meromorphicOrderAt_eq_int_iff (by fun_prop)] at *
+  obtain ⟨g, hg⟩ := hn
+  use -g
+  simp_all
+
+/-- The order of a function `f` equals the order of `-f`. -/
+theorem meromorphicOrderAt_fun_neg {f : 𝕜 → E} :
+    meromorphicOrderAt f x = meromorphicOrderAt (fun z ↦ -f z) x := meromorphicOrderAt_neg
+
 /-- The order is additive when multiplying scalar-valued and vector-valued meromorphic functions. -/
 @[to_fun] theorem meromorphicOrderAt_smul {f : 𝕜 → 𝕜} {g : 𝕜 → E}
     (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) :
diff --git a/Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean b/Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean
index 26e829688f..459e144ce2 100644
--- a/Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean
+++ b/Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean
@@ -196,6 +196,31 @@ lemma meromorphicTrailingCoeffAt_congr_nhdsNE {f₁ f₂ : 𝕜 → E} (h : f₁
 ## Behavior under Arithmetic Operations
 -/
 
+/--
+Taking the negative commutes with taking `meromorphicTrailingCoeffAt`.
+-/
+theorem meromorphicTrailingCoeffAt_neg {f : 𝕜 → E} :
+    meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x := by
+  by_cases h₁ : ¬ MeromorphicAt f x
+  · aesop
+  rw [not_not] at h₁
+  by_cases h₂ : meromorphicOrderAt f x = ⊤
+  · simp_all [← meromorphicOrderAt_neg]
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂
+  rw [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g h₃g]
+  rw [AnalyticAt.meromorphicTrailingCoeffAt_of_eq_nhdsNE (g := -g)]
+  · simp
+  · fun_prop
+  · filter_upwards [h₃g] with a ha
+    simp [ha, ← meromorphicOrderAt_neg]
+
+/--
+Taking the negative commutes with taking `meromorphicTrailingCoeffAt`.
+-/
+theorem meromorphicTrailingCoeffAt_fun_neg {f : 𝕜 → E} :
+    meromorphicTrailingCoeffAt (fun z ↦ -f z) x = -meromorphicTrailingCoeffAt f x :=
+  meromorphicTrailingCoeffAt_neg
+
 /--
 If `f₁` and `f₂` have unequal order at `x`, then the trailing coefficient of `f₁ + f₂` at `x` is the
 trailing coefficient of the function with the lowest order.
@@ -235,6 +260,35 @@ theorem MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_left_of_lt {f₁ f₂ :
     smul_eq_zero, zero_zpow _ (sub_ne_zero.2 (ne_of_lt h).symm)]
   tauto
 
+/--
+If `f₁` and `f₂` have unequal order at `x`, then the trailing coefficient of `f₁ + f₂` at `x` is the
+trailing coefficient of the function with the lowest order.
+-/
+theorem MeromorphicAt.meromorphicTrailingCoeffAt_fun_add_eq_left_of_lt {f₁ f₂ : 𝕜 → E}
+    (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) :
+    meromorphicTrailingCoeffAt (fun z ↦ f₁ z + f₂ z) x = meromorphicTrailingCoeffAt f₁ x :=
+  MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_left_of_lt hf₂ h
+
+/--
+If `f₁` and `f₂` have unequal order at `x`, then the trailing coefficient of `f₁ - f₂` at `x` is the
+trailing coefficient of the function with the lowest order.
+-/
+theorem MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_left_of_lt {f₁ f₂ : 𝕜 → E}
+    (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) :
+    meromorphicTrailingCoeffAt (f₁ - f₂) x = meromorphicTrailingCoeffAt f₁ x := by
+  rw [sub_eq_add_neg]
+  apply MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_left_of_lt (by fun_prop)
+  rwa [← meromorphicOrderAt_neg]
+
+/--
+If `f₁` and `f₂` have unequal order at `x`, then the trailing coefficient of `f₁ - f₂` at `x` is the
+trailing coefficient of the function with the lowest order.
+-/
+theorem MeromorphicAt.meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt {f₁ f₂ : 𝕜 → E}
+    (hf₂ : MeromorphicAt f₂ x) (h : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x) :
+    meromorphicTrailingCoeffAt (fun z ↦ f₁ z - f₂ z) x = meromorphicTrailingCoeffAt f₁ x :=
+  MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_left_of_lt hf₂ h
+
 /--
 If `f₁` and `f₂` have equal order at `x` and if their trailing coefficients do not cancel, then the
 trailing coefficient of `f₁ + f₂` at `x` is the sum of the trailing coefficients.
@@ -264,6 +318,45 @@ theorem MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_add {f₁ f₂ : 𝕜 
   simp [AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (by fun_prop)
     (by simp_all) τ₀]
 
+/--
+If `f₁` and `f₂` have equal order at `x` and if their trailing coefficients do not cancel, then the
+trailing coefficient of `f₁ + f₂` at `x` is the sum of the trailing coefficients.
+-/
+theorem MeromorphicAt.meromorphicTrailingCoeffAt_fun_add_eq_add {f₁ f₂ : 𝕜 → E}
+    (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x)
+    (h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x)
+    (h₂ : meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x ≠ 0) :
+    meromorphicTrailingCoeffAt (fun z ↦ f₁ z + f₂ z) x
+      = meromorphicTrailingCoeffAt f₁ x + meromorphicTrailingCoeffAt f₂ x :=
+  MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_add hf₁ hf₂ h₁ h₂
+
+/--
+If `f₁` and `f₂` have equal order at `x` and if their trailing coefficients do not cancel, then the
+trailing coefficient of `f₁ - f₂` at `x` is the sum of the trailing coefficients.
+-/
+theorem MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_sub {f₁ f₂ : 𝕜 → E}
+    (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x)
+    (h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x)
+    (h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0) :
+    meromorphicTrailingCoeffAt (f₁ - f₂) x
+      = meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x := by
+  rw [sub_eq_add_neg, hf₁.meromorphicTrailingCoeffAt_add_eq_add (by fun_prop)]
+  · rw [meromorphicTrailingCoeffAt_neg, sub_eq_add_neg]
+  · rwa [← meromorphicOrderAt_neg]
+  · rwa [meromorphicTrailingCoeffAt_neg, ←sub_eq_add_neg]
+
+/--
+If `f₁` and `f₂` have equal order at `x` and if their trailing coefficients do not cancel, then the
+trailing coefficient of `f₁ - f₂` at `x` is the sum of the trailing coefficients.
+-/
+theorem MeromorphicAt.meromorphicTrailingCoeffAt_fun_sub_eq_sub {f₁ f₂ : 𝕜 → E}
+    (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x)
+    (h₁ : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x)
+    (h₂ : meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x ≠ 0) :
+    meromorphicTrailingCoeffAt (fun z ↦ f₁ z - f₂ z) x
+      = meromorphicTrailingCoeffAt f₁ x - meromorphicTrailingCoeffAt f₂ x :=
+  MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_sub hf₁ hf₂ h₁ h₂
+
 /--
 The trailing coefficient of a scalar product is the scalar product of the trailing coefficients.
 -/
@@ -287,6 +380,15 @@ lemma MeromorphicAt.meromorphicTrailingCoeffAt_smul {f₁ : 𝕜 → 𝕜} {f₂
     (h₁g₁.smul h₁g₂).meromorphicTrailingCoeffAt_of_eq_nhdsNE this]
   simp
 
+/--
+The trailing coefficient of a scalar product is the scalar product of the trailing coefficients.
+-/
+lemma MeromorphicAt.meromorphicTrailingCoeffAt_fun_smul {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E}
+    (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) :
+    meromorphicTrailingCoeffAt (fun z ↦ f₁ z • f₂ z) x =
+      (meromorphicTrailingCoeffAt f₁ x) • (meromorphicTrailingCoeffAt f₂ x) :=
+  MeromorphicAt.meromorphicTrailingCoeffAt_smul hf₁ hf₂
+
 /--
 The trailing coefficient of a product is the product of the trailing coefficients.
 -/
@@ -296,6 +398,15 @@ lemma MeromorphicAt.meromorphicTrailingCoeffAt_mul {f₁ f₂ : 𝕜 → 𝕜} (
       (meromorphicTrailingCoeffAt f₁ x) * (meromorphicTrailingCoeffAt f₂ x) :=
   meromorphicTrailingCoeffAt_smul hf₁ hf₂
 
+/--
+The trailing coefficient of a product is the product of the trailing coefficients.
+-/
+lemma MeromorphicAt.meromorphicTrailingCoeffAt_fun_mul {f₁ f₂ : 𝕜 → 𝕜}
+    (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) :
+    meromorphicTrailingCoeffAt (fun z ↦ f₁ z * f₂ z) x =
+      (meromorphicTrailingCoeffAt f₁ x) * (meromorphicTrailingCoeffAt f₂ x) :=
+  meromorphicTrailingCoeffAt_smul hf₁ hf₂
+
 /--
 The trailing coefficient of a product is the product of the trailing coefficients.
 -/
@@ -314,6 +425,16 @@ theorem meromorphicTrailingCoeffAt_prod {ι : Type*} {s : Finset ι} {f : ι →
       (h σ (Finset.mem_insert_self σ s₁)).meromorphicTrailingCoeffAt_mul
       (MeromorphicAt.prod this), hind this]
 
+/--
+The trailing coefficient of a product is the product of the trailing coefficients.
+-/
+theorem meromorphicTrailingCoeffAt_fun_prod {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → 𝕜}
+    {x : 𝕜} (h : ∀ σ ∈ s, MeromorphicAt (f σ) x) :
+    meromorphicTrailingCoeffAt (fun z ↦ ∏ n ∈ s, f n z) x
+      = ∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x := by
+  convert meromorphicTrailingCoeffAt_prod h
+  simp
+
 /--
 The trailing coefficient of the inverse function is the inverse of the trailing coefficient.
 -/
@@ -333,6 +454,13 @@ lemma meromorphicTrailingCoeffAt_inv {f : 𝕜 → 𝕜} :
       exact eventuallyEq_nhdsWithin_of_eqOn fun _ ↦ congrFun rfl
   · simp_all
 
+/--
+The trailing coefficient of the inverse function is the inverse of the trailing coefficient.
+-/
+lemma meromorphicTrailingCoeffAt_fun_inv {f : 𝕜 → 𝕜} :
+    meromorphicTrailingCoeffAt (fun z ↦ (f z)⁻¹) x = (meromorphicTrailingCoeffAt f x)⁻¹ :=
+  meromorphicTrailingCoeffAt_inv
+
 /--
 The trailing coefficient of the power of a function is the power of the trailing coefficient.
 -/
@@ -356,6 +484,23 @@ lemma MeromorphicAt.meromorphicTrailingCoeffAt_zpow {n : ℤ} {f : 𝕜 → 𝕜
 /--
 The trailing coefficient of the power of a function is the power of the trailing coefficient.
 -/
-lemma MeromorphicAt.meromorphicTrailingCoeffAt_pow {n : ℕ} {f : 𝕜 → 𝕜} (h₁ : MeromorphicAt f x) :
+lemma MeromorphicAt.meromorphicTrailingCoeffAt_fun_zpow {n : ℤ} {f : 𝕜 → 𝕜}
+    (h₁ : MeromorphicAt f x) :
+    meromorphicTrailingCoeffAt (fun z ↦ f z ^ n) x = (meromorphicTrailingCoeffAt f x) ^ n :=
+  MeromorphicAt.meromorphicTrailingCoeffAt_zpow h₁
+
+/--
+The trailing coefficient of the power of a function is the power of the trailing coefficient.
+-/
+lemma MeromorphicAt.meromorphicTrailingCoeffAt_pow {n : ℕ} {f : 𝕜 → 𝕜}
+    (h₁ : MeromorphicAt f x) :
     meromorphicTrailingCoeffAt (f ^ n) x = (meromorphicTrailingCoeffAt f x) ^ n := by
   convert h₁.meromorphicTrailingCoeffAt_zpow (n := n) <;> simp
+
+/--
+The trailing coefficient of the power of a function is the power of the trailing coefficient.
+-/
+lemma MeromorphicAt.meromorphicTrailingCoeffAt_fun_pow {n : ℕ} {f : 𝕜 → 𝕜}
+    (h₁ : MeromorphicAt f x) :
+    meromorphicTrailingCoeffAt (fun z ↦ f z ^ n) x = (meromorphicTrailingCoeffAt f x) ^ n :=
+  MeromorphicAt.meromorphicTrailingCoeffAt_pow h₁
diff --git a/Mathlib/Topology/DiscreteSubset.lean b/Mathlib/Topology/DiscreteSubset.lean
index 2d2d24190d..63bf9246ff 100644
--- a/Mathlib/Topology/DiscreteSubset.lean
+++ b/Mathlib/Topology/DiscreteSubset.lean
@@ -298,6 +298,30 @@ theorem codiscreteWithin_iff_locallyFiniteComplementWithin [T1Space X] {s U : Se
     use t \ (t ∩ (U \ s)), nhdsNE_of_nhdsNE_sdiff_finite (mem_nhdsWithin_of_mem_nhds h₁t) h₂t
     simp
 
+/--
+In a `T1Space`, complements of singleton sets are codiscrete within any set.
+-/
+@[simp]
+theorem compl_singleton_mem_codiscreteWithin {X : Type*} [TopologicalSpace X] [T1Space X]
+    {s : Set X} (x : X) :
+    {x}ᶜ ∈ codiscreteWithin s := by
+  rw [codiscreteWithin_iff_locallyEmptyComplementWithin]
+  intro z hz
+  use univ \ {x}
+  exact ⟨nhdsNE_of_nhdsNE_sdiff_finite univ_mem Finite.of_subsingleton, by aesop⟩
+
+/--
+In a `T1Space`, complements of finite sets are codiscrete within any set.
+-/
+theorem compl_finite_mem_codiscreteWithin {X : Type*} [TopologicalSpace X] [T1Space X]
+    {s t : Set X} (h : t.Finite) :
+    tᶜ ∈ codiscreteWithin s := by
+  apply h.induction_on (motive := fun t _ ↦ tᶜ ∈ codiscreteWithin s)
+  · simp
+  · intro τ t hτ h₁t h₂t
+    have : (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ := by aesop
+    simp_all
+
 /-- In any topological space, the open sets with discrete complement form a filter,
 defined as the supremum of all punctured neighborhoods.
 

From c9f4f1b787897e4b33e9347a0856c50ca8fefe0c Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <5110976+kebekus@users.noreply.github.com>
Date: Sun, 10 May 2026 18:52:16 +0000
Subject: [PATCH 03/11] feat: variants of the principle of isolated zeros for
 meromorphic functions (#38984)

Add simple, but useful, variants of the principle of isolated zeros for meromorphic functions.
---
 Mathlib/Analysis/Meromorphic/IsolatedZeros.lean | 14 +++++++++++++-
 Mathlib/Analysis/Meromorphic/Order.lean         | 11 +++++++++++
 2 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Meromorphic/IsolatedZeros.lean b/Mathlib/Analysis/Meromorphic/IsolatedZeros.lean
index db23b63136..3773c08389 100644
--- a/Mathlib/Analysis/Meromorphic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Meromorphic/IsolatedZeros.lean
@@ -5,7 +5,7 @@ Authors: Stefan Kebekus
 -/
 module
 
-public import Mathlib.Analysis.Meromorphic.Basic
+public import Mathlib.Analysis.Meromorphic.Order
 
 /-!
 # Principles of Isolated Zeros and Identity Principles for Meromorphic Functions
@@ -64,6 +64,18 @@ theorem eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin (hf : Mer
     (mem_codiscreteWithin_iff_forall_mem_nhdsNE.1 h x h₁x)).mono
   simp +contextual
 
+/--
+Variant of the principle of isolated zeros, formulated in terms of orders: If `f` is nowhere locally
+constant zero, then its zero set is discrete within its domain of meromorphicity.
+-/
+theorem MeromorphicOn.codiscreteWithin_setOf_ne_zero (h₁f : MeromorphicOn f U)
+    (h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤) :
+    ∀ᶠ x in codiscreteWithin U, f x ≠ 0 := by
+  filter_upwards [h₁f.analyticAt_mem_codiscreteWithin,
+    h₁f.codiscreteWithin_setOf_meromorphicOrderAt_eq_zero_or_top h₂f] with x h₁x h₂x
+  have := h₂f x h₂x.1
+  simp_all [← h₁x.analyticOrderAt_eq_zero, h₁x.meromorphicOrderAt_eq]
+
 /-!
 ## Identity Principles
 -/
diff --git a/Mathlib/Analysis/Meromorphic/Order.lean b/Mathlib/Analysis/Meromorphic/Order.lean
index 6fe62f5a95..00c76cd85b 100644
--- a/Mathlib/Analysis/Meromorphic/Order.lean
+++ b/Mathlib/Analysis/Meromorphic/Order.lean
@@ -785,6 +785,17 @@ theorem codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top (hf : MeromorphicOn f
     · simp +contextual [h'.meromorphicOrderAt_eq, h'.analyticOrderAt_eq_zero.2, h'₁a]
     · exact fun ha ↦ (h' ha).elim
 
+/--
+Variant of `codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top`: The set where a meromorphic
+function has zero or infinite order is codiscrete within its domain of meromorphicity.
+-/
+theorem codiscreteWithin_setOf_meromorphicOrderAt_eq_zero_or_top (h₁f : MeromorphicOn f U)
+    (h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤) :
+    {u ∈ U | meromorphicOrderAt f u = 0 ∨ meromorphicOrderAt f u = ⊤} ∈ codiscreteWithin U := by
+  convert mem_codiscrete_subtype_iff_mem_codiscreteWithin.1
+    h₁f.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top
+  aesop
+
 end MeromorphicOn
 
 section comp

From 8ffbd01125653599f2025ec32adfb95a36285d7c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez=20Palacios?= <vi.hdz.p@gmail.com>
Date: Sun, 10 May 2026 19:17:37 +0000
Subject: [PATCH 04/11] =?UTF-8?q?feat(SetTheory):=20=E2=84=B5=5F=20univ=20?=
 =?UTF-8?q?=3D=20univ=20(#37545)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/SetTheory/Cardinal/Aleph.lean   | 17 +++++++
 Mathlib/SetTheory/Cardinal/Regular.lean | 63 ++++++++++++++++++++++---
 2 files changed, 73 insertions(+), 7 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Aleph.lean b/Mathlib/SetTheory/Cardinal/Aleph.lean
index ebbf3a7b6d..992f8c99f9 100644
--- a/Mathlib/SetTheory/Cardinal/Aleph.lean
+++ b/Mathlib/SetTheory/Cardinal/Aleph.lean
@@ -11,6 +11,8 @@ public import Mathlib.SetTheory.Cardinal.ENat
 public import Mathlib.SetTheory.Ordinal.Enum
 public import Mathlib.SetTheory.Ordinal.Univ
 
+import Mathlib.SetTheory.Ordinal.Principal
+
 /-!
 # Omega, aleph, and beth functions
 
@@ -271,6 +273,12 @@ theorem range_omega : range omega = {x | ω ≤ x ∧ IsInitial x} := by
 theorem mem_range_omega_iff {x : Ordinal} : x ∈ range omega ↔ ω ≤ x ∧ IsInitial x := by
   rw [range_omega, mem_setOf]
 
+theorem preOmega_of_omega0_sq_le {o : Ordinal} (ho : ω ^ 2 ≤ o) : preOmega o = ω_ o := by
+  rw [← opow_natCast] at ho
+  rw [omega_eq_preOmega, add_of_omega0_opow_le _ ho]
+  apply left_lt_opow one_lt_omega0
+  simp
+
 end Ordinal
 
 /-! ### Aleph cardinals -/
@@ -519,6 +527,9 @@ theorem aleph1_le_mk (α : Type*) [Uncountable α] : ℵ₁ ≤ #α := by
 theorem countable_iff_lt_aleph_one {α : Type*} (s : Set α) : s.Countable ↔ #s < ℵ₁ := by
   rw [lt_aleph_one_iff, le_aleph0_iff_set_countable]
 
+theorem preAleph_of_omega0_sq_le {o : Ordinal} (ho : ω ^ 2 ≤ o) : preAleph o = ℵ_ o := by
+  simpa [← ord_inj] using preOmega_of_omega0_sq_le ho
+
 end Cardinal
 
 /-! ### Beth cardinals -/
@@ -727,6 +738,12 @@ theorem isStrongLimit_beth {o : Ordinal} : IsStrongLimit (ℶ_ o) ↔ IsSuccPrel
 theorem lift_beth (o : Ordinal) : lift.{v} (ℶ_ o) = ℶ_ (Ordinal.lift.{v} o) := by
   rw [beth_eq_preBeth, beth_eq_preBeth, lift_preBeth, Ordinal.lift_add, lift_omega0]
 
+theorem preBeth_of_omega0_sq_le {o : Ordinal} (ho : ω ^ 2 ≤ o) : preBeth o = ℶ_ o := by
+  rw [← opow_natCast] at ho
+  rw [beth, add_of_omega0_opow_le _ ho]
+  apply left_lt_opow one_lt_omega0
+  simp
+
 /-! ### Simp lemmas with `lift` -/
 
 section lift
diff --git a/Mathlib/SetTheory/Cardinal/Regular.lean b/Mathlib/SetTheory/Cardinal/Regular.lean
index d552b46b5e..067fbec191 100644
--- a/Mathlib/SetTheory/Cardinal/Regular.lean
+++ b/Mathlib/SetTheory/Cardinal/Regular.lean
@@ -20,10 +20,6 @@ This file defines regular, singular, and inaccessible cardinals.
   its cofinality is smaller than itself.
 * `Cardinal.IsInaccessible c` means that `c` is strongly inaccessible:
   `ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit c`.
-
-## TODO
-
-* Prove more theorems on inaccessible cardinals.
 -/
 
 @[expose] public section
@@ -411,15 +407,68 @@ theorem IsInaccessible.isRegular (h : IsInaccessible c) : IsRegular c :=
 theorem IsInaccessible.isStrongLimit (h : IsInaccessible c) : IsStrongLimit c :=
   ⟨h.ne_zero, h.two_power_lt⟩
 
+theorem IsInaccessible.isSuccLimit {c : Cardinal} (h : IsInaccessible c) : IsSuccLimit c :=
+  h.isStrongLimit.isSuccLimit
+
 theorem isInaccessible_def : IsInaccessible c ↔ ℵ₀ < c ∧ IsRegular c ∧ IsStrongLimit c where
   mp h := ⟨h.aleph0_lt, h.isRegular, h.isStrongLimit⟩
   mpr := fun ⟨h₁, h₂, h₃⟩ ↦ ⟨h₁, h₂.2, h₃.two_power_lt⟩
 
--- Lean's foundations prove the existence of ℵ₀ many inaccessible cardinals
+/-- Lean's foundations prove the existence of `v` inaccessibles in universe `v`. -/
 theorem IsInaccessible.univ : IsInaccessible univ.{u, v} :=
   ⟨aleph0_lt_univ, by simp, IsStrongLimit.univ.two_power_lt⟩
 
--- TODO: prove that `IsInaccessible o.card` implies `IsInaccessible (ℵ_ o)` and
--- `IsInaccessible (ℶ_ o)`
+theorem IsInaccessible.preBeth_ord (hc : IsInaccessible c) : preBeth c.ord = c := by
+  apply (preBeth_strictMono.comp ord_strictMono).le_apply.antisymm'
+  apply (isNormal_preBeth.le_iff_forall_le (isSuccLimit_ord hc.aleph0_lt.le)).2
+  refine fun a ha ↦ le_of_lt ?_
+  induction a using WellFoundedLT.induction with | ind a IH
+  rw [preBeth]
+  apply lift_iSup_lt_of_lt_cof_ord _ _
+  · rwa [mk_Iio_ordinal, lift_lift, hc.isRegular.lift.cof_ord, lift_lt, ← lt_ord]
+  · rintro ⟨b, hb⟩
+    exact hc.isStrongLimit.two_power_lt <| IH _ hb (hb.trans ha)
+
+theorem IsInaccessible.beth_ord (hc : IsInaccessible c) : ℶ_ c.ord = c := by
+  rw [← preBeth_of_omega0_sq_le (le_of_lt _), hc.preBeth_ord]
+  rw [lt_ord, pow_two, card_mul, card_omega0, aleph0_mul_aleph0]
+  exact hc.aleph0_lt
+
+theorem IsInaccessible.preAleph_ord (hc : IsInaccessible c) : preAleph c.ord = c :=
+  ((preAleph_le_preBeth _).trans hc.preBeth_ord.le).antisymm
+    (preAleph.strictMono.comp ord_strictMono).le_apply
+
+theorem IsInaccessible.aleph_ord (hc : IsInaccessible c) : ℵ_ c.ord = c :=
+  ((aleph_le_beth _).trans hc.beth_ord.le).antisymm (aleph.strictMono.comp ord_strictMono).le_apply
+
+theorem IsInaccessible.preOmega_ord (hc : IsInaccessible c) : preOmega c.ord = c.ord := by
+  rw [← ord_preAleph, hc.preAleph_ord]
+
+theorem IsInaccessible.omega_ord (hc : IsInaccessible c) : ω_ c.ord = c.ord := by
+  rw [← ord_aleph, hc.aleph_ord]
+
+@[simp]
+theorem preBeth_univ : preBeth Ordinal.univ.{u, v} = univ.{u, v} := by
+  simpa using IsInaccessible.univ.preBeth_ord
+
+@[simp]
+theorem beth_univ : ℶ_ Ordinal.univ.{u, v} = univ.{u, v} := by
+  simpa using IsInaccessible.univ.beth_ord
+
+@[simp]
+theorem preAleph_univ : preAleph Ordinal.univ.{u, v} = univ.{u, v} := by
+  simpa using IsInaccessible.univ.preAleph_ord
+
+@[simp]
+theorem aleph_univ : ℵ_ Ordinal.univ.{u, v} = univ.{u, v} := by
+  simpa using IsInaccessible.univ.aleph_ord
+
+@[simp]
+theorem _root_.Ordinal.preOmega_univ : preOmega Ordinal.univ.{u, v} = Ordinal.univ.{u, v} := by
+  simpa using IsInaccessible.univ.preOmega_ord
+
+@[simp]
+theorem _root_.Ordinal.omega_univ : ω_ Ordinal.univ.{u, v} = Ordinal.univ.{u, v} := by
+  simpa using IsInaccessible.univ.omega_ord
 
 end Cardinal

From 84ac9e54e0db7d4dfdcdb64a13dc75a6a44d63e9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez=20Palacios?= <vi.hdz.p@gmail.com>
Date: Sun, 10 May 2026 19:57:43 +0000
Subject: [PATCH 05/11] chore: fix name of theorem in docstring (#39148)

Plus a small golf.
---
 Mathlib/SetTheory/Ordinal/FundamentalSequence.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/SetTheory/Ordinal/FundamentalSequence.lean b/Mathlib/SetTheory/Ordinal/FundamentalSequence.lean
index dac122e01d..18d98a4fb9 100644
--- a/Mathlib/SetTheory/Ordinal/FundamentalSequence.lean
+++ b/Mathlib/SetTheory/Ordinal/FundamentalSequence.lean
@@ -33,7 +33,7 @@ variable {a b o : Ordinal}
 cofinal range. We provide `a = o.cof.ord` explicitly to avoid type rewrites. -/
 structure IsFundamentalSeq (f : Iio a → Iio o) : Prop where
   /-- This condition alongside the others is enough to conclude `o.cof.ord = a`, see
-  `IsFundamentalSeq.ord_cof_eq`. -/
+  `IsFundamentalSeq.ord_cof`. -/
   le_ord_cof : a ≤ o.cof.ord
   /-- A fundamental sequence is strictly monotonic. -/
   strictMono : StrictMono f
@@ -75,7 +75,7 @@ protected theorem id (ho : o ≤ o.cof.ord) : IsFundamentalSeq (o := o) id where
 protected theorem zero (f : Iio 0 → Iio 0) : IsFundamentalSeq f where
   strictMono _ := by simp
   le_ord_cof := by simp
-  isCofinal_range := by rw [range_eq_empty, isCofinal_empty_iff]; infer_instance
+  isCofinal_range := .of_isEmpty _
 
 /-- The length one sequence `(o)` is a fundamental sequence for `o + 1`. -/
 protected theorem add_one (o : Ordinal) :

From 6fa62653504dc0a80be9b39ad4505e961d58d399 Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Sun, 10 May 2026 20:09:25 +0000
Subject: [PATCH 06/11] feat: add IsMulCommutative instances for directed
 families of commutative subobjects (#36553)

---
 .../Algebra/Algebra/NonUnitalSubalgebra.lean  | 12 +++++++
 .../Algebra/Algebra/Subalgebra/Directed.lean  | 11 ++++++
 Mathlib/Algebra/Group/Subgroup/Lattice.lean   | 17 +++++++++
 .../Algebra/Group/Submonoid/Membership.lean   | 17 +++++++++
 .../Group/Subsemigroup/Membership.lean        | 19 ++++++++++
 Mathlib/Algebra/Ring/Subring/Basic.lean       | 11 ++++++
 Mathlib/Algebra/Ring/Subsemiring/Basic.lean   | 11 ++++++
 Mathlib/Algebra/Star/NonUnitalSubalgebra.lean | 11 ++++++
 Mathlib/Algebra/Star/Subalgebra.lean          | 35 ++++++++++++++++++-
 .../RingTheory/NonUnitalSubring/Basic.lean    | 11 ++++++
 .../NonUnitalSubsemiring/Basic.lean           | 15 ++++++++
 11 files changed, 169 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
index a7b789bec4..c08efebd26 100644
--- a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
+++ b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
@@ -986,6 +986,18 @@ theorem coe_iSup_of_directed [Nonempty ι] {S : ι → NonUnitalSubalgebra R A}
     (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
   this.symm ▸ rfl
 
+theorem isMulCommutative_iSup {ι : Sort*} [Nonempty ι] {S : ι → NonUnitalSubalgebra R A}
+    [hS : ∀ i, IsMulCommutative (S i)] (dir : Directed (· ≤ ·) S) :
+    IsMulCommutative (⨆ i, S i : NonUnitalSubalgebra R A) := by
+  have := NonUnitalSubsemiring.isMulCommutative_iSup dir
+  simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
+    NonUnitalSubsemiring.coe_iSup_of_directed dir]
+
+instance instIsMulCommutative_iSup {ι : Type*} [Nonempty ι] [Preorder ι] [IsDirectedOrder ι]
+    {S : ι →o NonUnitalSubalgebra R A} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : NonUnitalSubalgebra R A) :=
+  isMulCommutative_iSup S.monotone.directed_le
+
 /-- Define an algebra homomorphism on a directed supremum of non-unital subalgebras by defining
 it on each non-unital subalgebra, and proving that it agrees on the intersection of
 non-unital subalgebras. -/
diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Directed.lean b/Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
index 04864c8ae9..9f7129dabe 100644
--- a/Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
+++ b/Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
@@ -38,6 +38,17 @@ theorem coe_iSup_of_directed (dir : Directed (· ≤ ·) K) : ↑(iSup K) = ⋃
     (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)
   simp [this, s]
 
+theorem isMulCommutative_iSup {S : ι → Subalgebra R A}
+    [hS : ∀ i, IsMulCommutative (S i)] (dir : Directed (· ≤ ·) S) :
+    IsMulCommutative (⨆ i, S i : Subalgebra R A) := by
+  simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
+    Subsemiring.coe_iSup_of_directed dir] using Subsemiring.isMulCommutative_iSup dir
+
+instance instIsMulCommutative_iSup [Preorder ι] [IsDirectedOrder ι]
+    {S : ι →o Subalgebra R A} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : Subalgebra R A) :=
+  isMulCommutative_iSup S.monotone.directed_le
+
 variable (K)
 
 /-- Define an algebra homomorphism on a directed supremum of subalgebras by defining
diff --git a/Mathlib/Algebra/Group/Subgroup/Lattice.lean b/Mathlib/Algebra/Group/Subgroup/Lattice.lean
index 9bf4efa5c3..d8cecbc566 100644
--- a/Mathlib/Algebra/Group/Subgroup/Lattice.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Lattice.lean
@@ -580,6 +580,23 @@ theorem mem_sSup_of_directedOn {K : Set (Subgroup G)} (Kne : K.Nonempty) (hK : D
   haveI : Nonempty K := Kne.to_subtype
   simp only [sSup_eq_iSup', mem_iSup_of_directed hK.directed_val, SetCoe.exists, exists_prop]
 
+@[to_additive]
+theorem isMulCommutative_iSup {ι : Sort*} [Nonempty ι]
+    {S : ι → Subgroup G} [hS : ∀ i, IsMulCommutative (S i)]
+    (dir : Directed (· ≤ ·) S) : IsMulCommutative (⨆ i, S i : Subgroup G) := by
+  refine .of_setLike_mul_comm ?_
+  simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
+    SetLike.mem_coe, forall_exists_index]
+  intro a i ha b j hb
+  obtain ⟨k, hik, hjk⟩ := dir i j
+  exact setLike_mul_comm (hik ha) (hjk hb)
+
+@[to_additive]
+instance instIsMulCommutative_iSup {ι : Type*} [Nonempty ι] [Preorder ι] [IsDirectedOrder ι]
+    {S : ι →o Subgroup G} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : Subgroup G) :=
+  isMulCommutative_iSup S.monotone.directed_le
+
 variable {C : Type*} [CommGroup C] {s t : Subgroup C} {x : C}
 
 @[to_additive]
diff --git a/Mathlib/Algebra/Group/Submonoid/Membership.lean b/Mathlib/Algebra/Group/Submonoid/Membership.lean
index 291a60b2a8..d54ccf60fc 100644
--- a/Mathlib/Algebra/Group/Submonoid/Membership.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Membership.lean
@@ -96,6 +96,23 @@ theorem coe_sSup_of_directedOn {S : Set (Submonoid M)} (Sne : S.Nonempty)
     (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set M) = ⋃ s ∈ S, ↑s :=
   Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]
 
+@[to_additive]
+theorem isMulCommutative_iSup {ι : Sort*} [Nonempty ι]
+    {S : ι → Submonoid M} [hS : ∀ i, IsMulCommutative (S i)]
+    (dir : Directed (· ≤ ·) S) : IsMulCommutative (⨆ i, S i : Submonoid M) := by
+  refine .of_setLike_mul_comm ?_
+  simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
+    SetLike.mem_coe, forall_exists_index]
+  intro a i ha b j hb
+  obtain ⟨k, hik, hjk⟩ := dir i j
+  exact setLike_mul_comm (hik ha) (hjk hb)
+
+@[to_additive]
+instance instIsMulCommutative_iSup {ι : Type*} [Nonempty ι] [Preorder ι]
+    [IsDirectedOrder ι] {S : ι →o Submonoid M} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : Submonoid M) :=
+  Submonoid.isMulCommutative_iSup S.monotone.directed_le
+
 @[to_additive]
 theorem mem_sup_left {S T : Submonoid M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T := by
   rw [← SetLike.le_def]
diff --git a/Mathlib/Algebra/Group/Subsemigroup/Membership.lean b/Mathlib/Algebra/Group/Subsemigroup/Membership.lean
index 9ff4e85674..4f4d75d3e3 100644
--- a/Mathlib/Algebra/Group/Subsemigroup/Membership.lean
+++ b/Mathlib/Algebra/Group/Subsemigroup/Membership.lean
@@ -79,6 +79,25 @@ theorem coe_iSup_of_directed {S : ι → Subsemigroup M} (hS : Directed (· ≤
     ((⨆ i, S i : Subsemigroup M) : Set M) = ⋃ i, S i :=
   Set.ext fun x => by simp [mem_iSup_of_directed hS]
 
+/-- The supremum of a directed family of commutative subsemigroups is commutative. -/
+@[to_additive]
+theorem isMulCommutative_iSup {S : ι → Subsemigroup M}
+    [hS : ∀ i, IsMulCommutative (S i)] (dir : Directed (· ≤ ·) S) :
+    IsMulCommutative (⨆ i, S i : Subsemigroup M) := by
+  refine .of_setLike_mul_comm ?_
+  simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
+    SetLike.mem_coe, forall_exists_index]
+  intro a i ha b j hb
+  obtain ⟨k, hik, hjk⟩ := dir i j
+  exact setLike_mul_comm (hik ha) (hjk hb)
+
+/-- The supremum of a directed family of commutative subsemigroups is commutative. -/
+@[to_additive]
+instance instIsMulCommutative_iSup {ι : Type*} [Preorder ι] [IsDirectedOrder ι]
+    (S : ι →o Subsemigroup M) [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : Subsemigroup M) :=
+  isMulCommutative_iSup S.monotone.directed_le
+
 @[to_additive]
 theorem mem_sSup_of_directed_on {S : Set (Subsemigroup M)} (hS : DirectedOn (· ≤ ·) S) {x : M} :
     x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s := by
diff --git a/Mathlib/Algebra/Ring/Subring/Basic.lean b/Mathlib/Algebra/Ring/Subring/Basic.lean
index a43cd0987c..609c968912 100644
--- a/Mathlib/Algebra/Ring/Subring/Basic.lean
+++ b/Mathlib/Algebra/Ring/Subring/Basic.lean
@@ -790,6 +790,17 @@ theorem coe_sSup_of_directedOn {S : Set (Subring R)} (Sne : S.Nonempty)
     (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
   Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]
 
+theorem isMulCommutative_iSup {ι : Sort*} [Nonempty ι] {S : ι → Subring R}
+    [hS : ∀ i, IsMulCommutative (S i)] (dir : Directed (· ≤ ·) S) :
+    IsMulCommutative (⨆ i, S i : Subring R) := by
+  simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
+    Subsemigroup.coe_iSup_of_directed dir] using Subsemigroup.isMulCommutative_iSup dir
+
+instance instIsMulCommutative_iSup {ι : Type*} [Nonempty ι] [Preorder ι] [IsDirectedOrder ι]
+    {S : ι →o Subring R} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : Subring R) :=
+  Subring.isMulCommutative_iSup S.monotone.directed_le
+
 theorem mem_map_equiv {f : R ≃+* S} {K : Subring R} {x : S} :
     x ∈ K.map (f : R →+* S) ↔ f.symm x ∈ K :=
   @Set.mem_image_equiv _ _ (K : Set R) f.toEquiv x
diff --git a/Mathlib/Algebra/Ring/Subsemiring/Basic.lean b/Mathlib/Algebra/Ring/Subsemiring/Basic.lean
index aeca400a57..e49a70e64d 100644
--- a/Mathlib/Algebra/Ring/Subsemiring/Basic.lean
+++ b/Mathlib/Algebra/Ring/Subsemiring/Basic.lean
@@ -691,6 +691,17 @@ theorem coe_sSup_of_directedOn {S : Set (Subsemiring R)} (Sne : S.Nonempty)
     (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
   Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]
 
+theorem isMulCommutative_iSup {ι : Sort*} [Nonempty ι]
+    {S : ι → Subsemiring R} [hS : ∀ i, IsMulCommutative (S i)]
+    (dir : Directed (· ≤ ·) S) : IsMulCommutative (⨆ i, S i : Subsemiring R) := by
+  simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
+    Subsemigroup.coe_iSup_of_directed dir] using Subsemigroup.isMulCommutative_iSup dir
+
+instance instIsMulCommutative_iSup {ι : Type*} [Nonempty ι] [Preorder ι] [IsDirectedOrder ι]
+    {S : ι →o Subsemiring R} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : Subsemiring R) :=
+  isMulCommutative_iSup S.monotone.directed_le
+
 end Subsemiring
 
 namespace RingHom
diff --git a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
index 03cdc59146..57667d6696 100644
--- a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
+++ b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
@@ -1037,6 +1037,17 @@ theorem coe_iSup_of_directed [Nonempty ι] {S : ι → NonUnitalStarSubalgebra R
     (Set.iUnion_subset fun _ ↦ le_iSup S _)
   this.symm ▸ rfl
 
+theorem isMulCommutative_iSup [Nonempty ι] {S : ι → NonUnitalStarSubalgebra R A}
+    [hS : ∀ i, IsMulCommutative (S i)] (dir : Directed (· ≤ ·) S) :
+    IsMulCommutative (⨆ i, S i : NonUnitalStarSubalgebra R A) := by
+  simpa [isMulCommutative_iff, ← SetLike.mem_coe, NonUnitalSubsemiring.coe_iSup_of_directed dir,
+    coe_iSup_of_directed dir] using NonUnitalSubsemiring.isMulCommutative_iSup dir
+
+instance instIsMulCommutative_iSup [Nonempty ι] [Preorder ι] [IsDirectedOrder ι]
+    {S : ι →o NonUnitalStarSubalgebra R A} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : NonUnitalStarSubalgebra R A) :=
+  isMulCommutative_iSup S.monotone.directed_le
+
 /-- Define a non-unital star algebra homomorphism on a directed supremum of non-unital star
 subalgebras by defining it on each non-unital star subalgebra, and proving that it agrees on the
 intersection of non-unital star subalgebras. -/
diff --git a/Mathlib/Algebra/Star/Subalgebra.lean b/Mathlib/Algebra/Star/Subalgebra.lean
index dba839b99c..5c70c3f315 100644
--- a/Mathlib/Algebra/Star/Subalgebra.lean
+++ b/Mathlib/Algebra/Star/Subalgebra.lean
@@ -5,7 +5,7 @@ Authors: Kim Morrison, Jireh Loreaux
 -/
 module
 
-public import Mathlib.Algebra.Algebra.Subalgebra.Lattice
+public import Mathlib.Algebra.Algebra.Subalgebra.Directed
 public import Mathlib.Algebra.Algebra.Tower
 public import Mathlib.Algebra.Star.Module
 public import Mathlib.Algebra.Star.NonUnitalSubalgebra
@@ -926,3 +926,36 @@ lemma StarAlgebra.adjoin_nonUnitalStarSubalgebra (s : Set A) :
   le_antisymm
     (adjoin_le <| NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin R s)
     (adjoin_le <| (NonUnitalStarAlgebra.subset_adjoin R s).trans <| subset_adjoin R _)
+
+namespace StarSubalgebra
+
+section directed
+
+variable {R}
+
+theorem coe_iSup_of_directed {ι : Type*} [Nonempty ι] {S : ι → StarSubalgebra R A}
+    (dir : Directed (· ≤ ·) S) : ↑(iSup S) = ⋃ i, (S i : Set A) :=
+  let K : StarSubalgebra R A :=
+    { __ := NonUnitalStarSubalgebra.copy _ _ (NonUnitalStarSubalgebra.coe_iSup_of_directed
+        (S := fun i ↦ (S i).toNonUnitalStarSubalgebra) dir).symm
+      algebraMap_mem' x :=
+        let ⟨i⟩ := ‹Nonempty ι›
+        Set.mem_iUnion.mpr ⟨i, algebraMap_mem (S i) x⟩ }
+  have : iSup S = K := le_antisymm (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set A)) i)
+    (Set.iUnion_subset fun _ ↦ le_iSup S _)
+  this.symm ▸ rfl
+
+theorem isMulCommutative_iSup {ι : Type*} [Nonempty ι] {S : ι → StarSubalgebra R A}
+    [hS : ∀ i, IsMulCommutative (S i)] (dir : Directed (· ≤ ·) S) :
+    IsMulCommutative (⨆ i, S i : StarSubalgebra R A) := by
+  simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
+    Subalgebra.coe_iSup_of_directed dir] using Subalgebra.isMulCommutative_iSup dir
+
+instance instIsMulCommutative_iSup {ι : Type*} [Nonempty ι] [Preorder ι] [IsDirectedOrder ι]
+    {S : ι →o StarSubalgebra R A} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : StarSubalgebra R A) :=
+  isMulCommutative_iSup S.monotone.directed_le
+
+end directed
+
+end StarSubalgebra
diff --git a/Mathlib/RingTheory/NonUnitalSubring/Basic.lean b/Mathlib/RingTheory/NonUnitalSubring/Basic.lean
index 71abede391..4d1d512b85 100644
--- a/Mathlib/RingTheory/NonUnitalSubring/Basic.lean
+++ b/Mathlib/RingTheory/NonUnitalSubring/Basic.lean
@@ -701,6 +701,17 @@ theorem coe_sSup_of_directedOn {S : Set (NonUnitalSubring R)} (Sne : S.Nonempty)
     (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
   Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]
 
+theorem isMulCommutative_iSup {ι : Sort*} [Nonempty ι] {S : ι → NonUnitalSubring R}
+    [hS : ∀ i, IsMulCommutative (S i)] (dir : Directed (· ≤ ·) S) :
+    IsMulCommutative (⨆ i, S i : NonUnitalSubring R) := by
+  simpa [isMulCommutative_iff, ← SetLike.mem_coe, NonUnitalSubsemiring.coe_iSup_of_directed dir,
+    coe_iSup_of_directed dir] using NonUnitalSubsemiring.isMulCommutative_iSup dir
+
+instance instIsMulCommutative_iSup {ι : Type*} [Nonempty ι] [Preorder ι] [IsDirectedOrder ι]
+    {S : ι →o NonUnitalSubring R} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : NonUnitalSubring R) :=
+  isMulCommutative_iSup S.monotone.directed_le
+
 theorem mem_map_equiv {f : R ≃+* S} {K : NonUnitalSubring R} {x : S} :
     x ∈ K.map (f : R →ₙ+* S) ↔ f.symm x ∈ K :=
   @Set.mem_image_equiv _ _ (K : Set R) f.toEquiv x
diff --git a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
index d72edde597..aa2d134443 100644
--- a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
+++ b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
@@ -635,6 +635,21 @@ theorem coe_sSup_of_directedOn {S : Set (NonUnitalSubsemiring R)} (Sne : S.Nonem
     (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
   Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]
 
+theorem isMulCommutative_iSup {ι : Sort*} [Nonempty ι]
+    {S : ι → NonUnitalSubsemiring R} [hS : ∀ i, IsMulCommutative (S i)]
+    (dir : Directed (· ≤ ·) S) : IsMulCommutative (⨆ i, S i : NonUnitalSubsemiring R) := by
+  refine .of_setLike_mul_comm ?_
+  simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
+    SetLike.mem_coe, forall_exists_index]
+  intro a i ha b j hb
+  obtain ⟨k, hik, hjk⟩ := dir i j
+  exact setLike_mul_comm (hik ha) (hjk hb)
+
+instance instIsMulCommutative_iSup {ι : Type*} [Nonempty ι] [Preorder ι]
+    [IsDirectedOrder ι] {S : ι →o NonUnitalSubsemiring R} [hS : ∀ i, IsMulCommutative (S i)] :
+    IsMulCommutative (⨆ i, S i : NonUnitalSubsemiring R) :=
+  NonUnitalSubsemiring.isMulCommutative_iSup S.monotone.directed_le
+
 end NonUnitalSubsemiring
 
 namespace NonUnitalRingHom

From 76a162dd77cc8c8b4c9eba6e548707dd1a917fae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez=20Palacios?= <vi.hdz.p@gmail.com>
Date: Sun, 10 May 2026 20:52:23 +0000
Subject: [PATCH 07/11] feat(SetTheory/Ordinal/Exponential): characterization
 of `a ^ b = 1` (#36891)

Used in the CGT repo.

Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
---
 Mathlib/SetTheory/Ordinal/Exponential.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Mathlib/SetTheory/Ordinal/Exponential.lean b/Mathlib/SetTheory/Ordinal/Exponential.lean
index 14e877229e..85e800cddc 100644
--- a/Mathlib/SetTheory/Ordinal/Exponential.lean
+++ b/Mathlib/SetTheory/Ordinal/Exponential.lean
@@ -150,6 +150,18 @@ theorem one_lt_opow {a b : Ordinal} : 1 < a ^ b ↔ 1 < a ∧ b ≠ 0 := by
 theorem one_lt_pow {a : Ordinal} {n : ℕ} : 1 < a ^ n ↔ 1 < a ∧ n ≠ 0 :=
   mod_cast one_lt_opow (b := n)
 
+@[simp]
+theorem opow_eq_one_iff {a b : Ordinal} : a ^ b = 1 ↔ a = 1 ∨ b = 0 := by
+  refine ⟨fun h ↦ ?_, by simp +contextual [or_imp]⟩
+  contrapose! h
+  obtain ha | ha := le_or_gt a 1
+  · simp_all [le_one_iff]
+  · simpa using ((opow_lt_opow_iff_right ha).2 h.2.pos).ne'
+
+@[simp]
+theorem pow_eq_one_iff {a : Ordinal} {n : ℕ} : a ^ n = 1 ↔ a = 1 ∨ n = 0 :=
+  mod_cast opow_eq_one_iff (b := n)
+
 theorem isSuccLimit_opow {a b : Ordinal} (a1 : 1 < a) : IsSuccLimit b → IsSuccLimit (a ^ b) :=
   (isNormal_opow a1).map_isSuccLimit
 

From 0bb58f289c03af79bde4c942fc2285aa1e3f06f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez=20Palacios?= <vi.hdz.p@gmail.com>
Date: Sun, 10 May 2026 20:52:25 +0000
Subject: [PATCH 08/11] feat: `Order.cof Ordinal = univ` (#37675)

---
 Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
index 84be4fadcd..8314a2fe85 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
@@ -558,6 +558,17 @@ theorem cof_univ : cof univ.{u, v} = Cardinal.univ.{u, v} := by
     ← not_bddAbove_iff_isCofinal]
   exact fun s hs ↦ mk_le_of_injective (enumOrdOrderIso s hs).injective
 
+@[simp]
+theorem _root_.Order.cof_ordinal : Order.cof Ordinal.{u} = Cardinal.univ.{u, u + 1} := by
+  have := (OrderIso.ofRelIsoLT liftPrincipalSeg.subrelIso.{u, u + 1}).lift_cof_congr
+  rw [Cardinal.lift_id'.{_, u + 2}] at this
+  change Order.cof (Iio univ) = _ at this
+  rwa [cof_Iio, ← lift_cof, Cardinal.lift_inj, cof_univ, eq_comm] at this
+
+@[simp]
+theorem _root_.Order.cof_cardinal : Order.cof Cardinal.{u} = Cardinal.univ.{u, u + 1} := by
+  rw [← preAleph.cof_congr, cof_ordinal]
+
 end Ordinal
 
 namespace Cardinal

From 1cb172ef448192dd800f1825f384ca690f530301 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sun, 10 May 2026 22:04:42 +0000
Subject: [PATCH 09/11] feat(Algebra/Order): stronger positivity criterion for
 `expect` (#38794)

From AddCombi
---
 .../Algebra/Order/BigOperators/Expect.lean    | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Algebra/Order/BigOperators/Expect.lean b/Mathlib/Algebra/Order/BigOperators/Expect.lean
index a3e8e1ca6b..440665a2a5 100644
--- a/Mathlib/Algebra/Order/BigOperators/Expect.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Expect.lean
@@ -110,15 +110,12 @@ end OrderedAddCommMonoid
 
 section OrderedCancelAddCommMonoid
 variable [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [Module ℚ≥0 α]
-  {a : α} {s : Finset ι} {f g : ι → α}
-section PosSMulStrictMono
-variable [PosSMulStrictMono ℚ≥0 α]
+  [PosSMulStrictMono ℚ≥0 α] {s : Finset ι} {f g : ι → α} {a : α}
 
-lemma expect_lt_expect (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
-    𝔼 i ∈ s, f i < 𝔼 i ∈ s, g i := by
-  apply smul_lt_smul_of_pos_left (sum_lt_sum hle hlt)
-  rw [inv_pos, Nat.cast_pos, card_pos]
-  exact hlt.imp (fun _ => And.left)
+lemma expect_lt_expect (hfg : ∀ i ∈ s, f i ≤ g i) (hfg' : ∃ i ∈ s, f i < g i) :
+    𝔼 i ∈ s, f i < 𝔼 i ∈ s, g i :=
+  smul_lt_smul_of_pos_left (sum_lt_sum hfg hfg')
+    (by obtain ⟨i, hi, -⟩ := hfg'; have : s.Nonempty := ⟨i, hi⟩; simpa)
 
 lemma expect_lt (hle : ∀ x ∈ s, f x ≤ a) (hlt : ∃ x ∈ s, f x < a) :
     𝔼 i ∈ s, f i < a := by
@@ -130,10 +127,12 @@ lemma lt_expect (hle : ∀ x ∈ s, a ≤ f x) (hlt : ∃ x ∈ s, a < f x) :
   rw [← expect_const (hlt.imp (fun _ => And.left)) a]
   exact expect_lt_expect hle hlt
 
+lemma expect_pos' (h : ∀ i ∈ s, 0 ≤ f i) (hs : ∃ i ∈ s, 0 < f i) : 0 < 𝔼 i ∈ s, f i :=
+  (expect_const_zero _).symm.trans_lt <| expect_lt_expect h hs
+
 lemma expect_pos (hf : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) : 0 < 𝔼 i ∈ s, f i :=
   smul_pos (inv_pos.2 <| mod_cast hs.card_pos) <| sum_pos hf hs
 
-end PosSMulStrictMono
 end OrderedCancelAddCommMonoid
 
 section LinearOrderedAddCommMonoid
@@ -235,7 +234,7 @@ meta def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do
       assumeInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
       return some
-        q(@expect_pos $ι $α $instα $pα $pα' $instmod $s $f $instαordsmul (fun i _ ↦ $pr i) $ps))
+        q(@expect_pos $ι $α $instα $pα $pα' $instmod $instαordsmul $s $f (fun i _ ↦ $pr i) $ps))
     -- Try to show that the sum is positive
     if let some p_pos := p_pos then
       return .positive p_pos

From 090daf0bfb88e400f2ccf57eb42bee5e25e6ee71 Mon Sep 17 00:00:00 2001
From: Sharvil Kesarwani <sharkesa@gmail.com>
Date: Sun, 10 May 2026 22:27:19 +0000
Subject: [PATCH 10/11] refactor(Topology/Algebra/Module/LinearMap): rename
 subtypeL companion lemmas (#38962)

This PR renames the companion lemmas of `Submodule.subtypeL` for consistency with `Submodule.mkQL` (introduced in PR #38811). Specifically, `Submodule.coe_subtypeL` is renamed to `Submodule.toLinearMap_subtypeL` (to accurately reflect that it projects to the underlying LinearMap, not a function-level coercion), and `Submodule.coe_subtypeL'` is renamed to `Submodule.coe_subtypeL` (since this is the genuine function-level coercion lemma).
---
 Mathlib/Analysis/Calculus/Implicit.lean       |  4 +-
 Mathlib/Analysis/Normed/Operator/Banach.lean  |  7 +--
 .../Topology/Algebra/Module/LinearMap.lean    | 58 +++++++++++--------
 scripts/nolints_prime_decls.txt               |  1 -
 4 files changed, 38 insertions(+), 32 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/Implicit.lean b/Mathlib/Analysis/Calculus/Implicit.lean
index 61a2502dc5..6ec8a5cd2b 100644
--- a/Mathlib/Analysis/Calculus/Implicit.lean
+++ b/Mathlib/Analysis/Calculus/Implicit.lean
@@ -428,11 +428,11 @@ theorem to_implicitFunctionOfComplemented (hf : HasStrictFDerivAt f f' a) (hf' :
   swap
   · ext
     simp only [Classical.choose_spec hker, implicitFunctionDataOfComplemented,
-      ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL', Submodule.coe_subtype,
+      ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL, Submodule.coe_subtype,
       ContinuousLinearMap.id_apply]
   swap
   · ext
-    simp only [ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL', Submodule.coe_subtype,
+    simp only [ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL, Submodule.coe_subtype,
       ContinuousLinearMap.apply_val_ker, ContinuousLinearMap.zero_apply]
   simp only [implicitFunctionDataOfComplemented, map_sub, sub_self]
 
diff --git a/Mathlib/Analysis/Normed/Operator/Banach.lean b/Mathlib/Analysis/Normed/Operator/Banach.lean
index 8d29a439d9..1f605499a8 100644
--- a/Mathlib/Analysis/Normed/Operator/Banach.lean
+++ b/Mathlib/Analysis/Normed/Operator/Banach.lean
@@ -498,10 +498,9 @@ noncomputable def coprodSubtypeLEquivOfIsCompl {F : Type*} [NormedAddCommGroup F
   ContinuousLinearEquiv.ofBijective (f.coprod G.subtypeL)
     (by
       rw [ker_coprod_of_disjoint_range]
-      · rw [hker, Submodule.ker_subtypeL, Submodule.prod_bot]
-      · rw [Submodule.range_subtypeL]
-        exact h.disjoint)
-    (by simp only [range_coprod, Submodule.range_subtypeL, h.sup_eq_top])
+      · simp [hker]
+      · simp [h.disjoint])
+    (by simp [LinearMap.range_coprod, h.sup_eq_top])
 
 theorem range_eq_map_coprodSubtypeLEquivOfIsCompl {F : Type*} [NormedAddCommGroup F]
     [NormedSpace 𝕜 F] [CompleteSpace F] (f : E →L[𝕜] F) {G : Submodule 𝕜 F}
diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean
index f88a40edfb..9e10ba35a0 100644
--- a/Mathlib/Topology/Algebra/Module/LinearMap.lean
+++ b/Mathlib/Topology/Algebra/Module/LinearMap.lean
@@ -702,31 +702,6 @@ theorem coe_rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂]
       (f : M₁ →ₛₗ[σ₁₂] M₂).rangeRestrict :=
   rfl
 
-/-- `Submodule.subtype` as a `ContinuousLinearMap`. -/
-def _root_.Submodule.subtypeL (p : Submodule R₁ M₁) : p →L[R₁] M₁ where
-  cont := continuous_subtype_val
-  toLinearMap := p.subtype
-
-@[simp, norm_cast]
-theorem _root_.Submodule.coe_subtypeL (p : Submodule R₁ M₁) :
-    (p.subtypeL : p →ₗ[R₁] M₁) = p.subtype :=
-  rfl
-
-@[simp]
-theorem _root_.Submodule.coe_subtypeL' (p : Submodule R₁ M₁) : ⇑p.subtypeL = p.subtype :=
-  rfl
-
-@[simp]
-theorem _root_.Submodule.subtypeL_apply (p : Submodule R₁ M₁) (x : p) : p.subtypeL x = x :=
-  rfl
-
-theorem _root_.Submodule.range_subtypeL (p : Submodule R₁ M₁) :
-    range (p.subtypeL : p →ₗ[R₁] M₁) = p :=
-  Submodule.range_subtype _
-
-theorem _root_.Submodule.ker_subtypeL (p : Submodule R₁ M₁) : ker (p.subtypeL : p →ₗ[R₁] M₁) = ⊥ :=
-  Submodule.ker_subtype _
-
 section
 
 variable {R S : Type*} [Semiring R] [Semiring S] [Module R M₁] [Module R M₂] [Module R S]
@@ -1258,6 +1233,37 @@ end ContinuousLinearMap
 
 namespace Submodule
 
+section Semiring
+
+variable {R : Type*} [Semiring R] {M : Type*} [TopologicalSpace M] [AddCommMonoid M] [Module R M]
+
+/-- `Submodule.subtype` as a `ContinuousLinearMap`. -/
+def subtypeL (p : Submodule R M) : p →L[R] M where
+  toLinearMap := p.subtype
+
+@[simp, norm_cast]
+theorem toLinearMap_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M) = p.subtype := rfl
+
+@[simp]
+theorem coe_subtypeL (p : Submodule R M) : ⇑p.subtypeL = p.subtype := rfl
+
+@[deprecated (since := "2026-05-06")]
+alias coe_subtypeL' := coe_subtypeL
+
+theorem subtypeL_apply (p : Submodule R M) (x : p) : p.subtypeL x = x := by simp
+
+@[deprecated range_subtype (since := "2026-05-06")]
+theorem range_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M).range = p :=
+  Submodule.range_subtype _
+
+@[deprecated ker_subtype (since := "2026-05-06")]
+theorem ker_subtypeL (p : Submodule R M) : (p.subtypeL : p →ₗ[R] M).ker = ⊥ :=
+  Submodule.ker_subtype _
+
+end Semiring
+
+section Ring
+
 variable {R : Type*} [Ring R] {M : Type*} [TopologicalSpace M] [AddCommGroup M] [Module R M]
   (S : Submodule R M)
 
@@ -1281,6 +1287,8 @@ theorem isQuotientMap_mkQL : IsQuotientMap S.mkQL := isQuotientMap_quot_mk
 theorem isOpenQuotientMap_mkQL [ContinuousAdd M] : IsOpenQuotientMap S.mkQL :=
   S.isOpenQuotientMap_mkQ
 
+end Ring
+
 end Submodule
 
 namespace ContinuousLinearMap
diff --git a/scripts/nolints_prime_decls.txt b/scripts/nolints_prime_decls.txt
index 7f888f2c10..b51046ee80 100644
--- a/scripts/nolints_prime_decls.txt
+++ b/scripts/nolints_prime_decls.txt
@@ -4144,7 +4144,6 @@ Sublattice.coe_inf'
 SubmoduleClass.module'
 Submodule.coe_continuous_linearProjOfClosedCompl'
 Submodule.coe_prodEquivOfIsCompl'
-Submodule.coe_subtypeL'
 Submodule.comap_smul'
 Submodule.disjoint_def'
 Submodule.disjoint_span_singleton'

From 50f0559af90cecbf1ed7cf4459565c7168329903 Mon Sep 17 00:00:00 2001
From: Anatole Dedecker <anatolededecker@gmail.com>
Date: Sun, 10 May 2026 22:54:31 +0000
Subject: [PATCH 11/11] feat: generalize
 Submodule.ClosedComplemented.of_quotient_finiteDimensional (#38579)

`Submodule.ClosedComplemented.of_quotient_finiteDimensional` currently says that any finite codimension *closed* subspace of a Banach space is topologically complemented. The current proof uses the Banach open mapping theorem.

In fact the result holds for any TVS over a nontrivially normed field, and we have the stronger result that any algebraic complement of a finite codimension closed subspace is in fact a topological complement.
---
 .../Analysis/Normed/Module/Complemented.lean  | 19 --------
 .../Algebra/Module/FiniteDimension.lean       | 43 +++++++++++++++++++
 2 files changed, 43 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/Complemented.lean b/Mathlib/Analysis/Normed/Module/Complemented.lean
index 97af27eb48..9e92be0d11 100644
--- a/Mathlib/Analysis/Normed/Module/Complemented.lean
+++ b/Mathlib/Analysis/Normed/Module/Complemented.lean
@@ -35,19 +35,6 @@ open LinearMap (ker range)
 
 namespace ContinuousLinearMap
 
-section
-
-variable [CompleteSpace 𝕜]
-
-theorem ker_closedComplemented_of_finiteDimensional_range (f : E →L[𝕜] F)
-    [FiniteDimensional 𝕜 f.range] : f.ker.ClosedComplemented := by
-  set f' : E →L[𝕜] f.range := f.codRestrict _ (LinearMap.mem_range_self (f : E →ₗ[𝕜] F))
-  rcases f'.exists_rightInverse_of_surjective (f : E →ₗ[𝕜] F).range_rangeRestrict with ⟨g, hg⟩
-  simpa only [f', ker_codRestrict]
-    using f'.closedComplemented_ker_of_rightInverse g (ContinuousLinearMap.ext_iff.1 hg)
-
-end
-
 variable [CompleteSpace E] [CompleteSpace (F × G)]
 
 /-- If `f : E →L[R] F` and `g : E →L[R] G` are two surjective linear maps and
@@ -127,10 +114,4 @@ theorem closedComplemented_iff_isClosed_exists_isClosed_isCompl :
   ⟨fun h => ⟨h.isClosed, h.exists_isClosed_isCompl⟩,
     fun ⟨hp, ⟨_, hq, hpq⟩⟩ => .of_isCompl_isClosed hpq hp hq⟩
 
-theorem ClosedComplemented.of_quotient_finiteDimensional [CompleteSpace 𝕜]
-    [FiniteDimensional 𝕜 (E ⧸ p)] (hp : IsClosed (p : Set E)) : p.ClosedComplemented := by
-  obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
-  haveI : FiniteDimensional 𝕜 q := (p.quotientEquivOfIsCompl q hq).finiteDimensional
-  exact .of_isCompl_isClosed hq hp q.closed_of_finiteDimensional
-
 end Submodule
diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean
index 8d5d7a7880..ae908df224 100644
--- a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean
+++ b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean
@@ -14,6 +14,7 @@ public import Mathlib.RingTheory.LocalRing.Basic
 public import Mathlib.Topology.Algebra.Module.Determinant
 public import Mathlib.Topology.Algebra.Module.ModuleTopology
 public import Mathlib.Topology.Algebra.Module.Simple
+public import Mathlib.Topology.Algebra.Module.Complement
 public import Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional
 public import Mathlib.Topology.Maps.Strict.Basic
 
@@ -704,3 +705,45 @@ theorem HasCompactMulSupport.eq_one_or_finiteDimensional {X : Type*} [Topologica
   HasCompactSupport.eq_zero_or_finiteDimensional 𝕜 (X := Additive X) hf h'f
 
 end Riesz
+
+section Compl
+
+open Submodule
+
+/-- If `p` is a closed subspace with finite codimension, then any algebraic complement `q` to `p`
+is a topological complement. -/
+theorem Submodule.IsCompl.isTopCompl_of_finiteDimensional_quotient {p q : Submodule 𝕜 E}
+    (h : IsCompl p q) (hp : IsClosed (p : Set E)) [FiniteDimensional 𝕜 (E ⧸ p)] :
+    IsTopCompl p q := by
+  let φ : E ⧸ p →L[𝕜] q := (p.quotientEquivOfIsCompl q h).toLinearMap.toContinuousLinearMap
+  have := (φ ∘L p.mkQL).isTopCompl_of_proj fun x ↦ by simp [φ]
+  simpa [φ] using this.symm
+
+/-- Assume that `p q : Submodule 𝕜 E` are algebraic complements. If `p` is closed and `q`
+has finite dimension, then they are in fact topological complements.
+
+Note that this theorem does not help you to build a closed complement to a finite dimensional
+subspace. That requires the Hahn-Banach theorem, and you don't get much control over what the
+complement is. See `Submodule.ClosedComplemented.of_finiteDimensional`. -/
+theorem Submodule.IsCompl.isTopCompl_of_isClosed_of_finiteDimensional {p q : Submodule 𝕜 E}
+    (h : IsCompl p q) (hp : IsClosed (p : Set E)) [hq : FiniteDimensional 𝕜 q] :
+    IsTopCompl p q := by
+  suffices FiniteDimensional 𝕜 (E ⧸ p) from h.isTopCompl_of_finiteDimensional_quotient hp
+  exact (p.quotientEquivOfIsCompl q h).symm.finiteDimensional
+
+theorem Submodule.ClosedComplemented.of_finiteDimensional_quotient {p : Submodule 𝕜 E}
+    (hp : IsClosed (p : Set E)) [hq : FiniteDimensional 𝕜 (E ⧸ p)] : p.ClosedComplemented := by
+  obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
+  exact hq.isTopCompl_of_finiteDimensional_quotient hp |>.closedComplemented
+
+@[deprecated (since := "2026-05-09")]
+alias Submodule.ClosedComplemented.of_quotient_finiteDimensional :=
+  Submodule.ClosedComplemented.of_finiteDimensional_quotient
+
+omit [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] in
+theorem ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range [T2Space F]
+    (f : E →L[𝕜] F) [FiniteDimensional 𝕜 f.range] : f.ker.ClosedComplemented := by
+  suffices FiniteDimensional 𝕜 (E ⧸ f.ker) from .of_finiteDimensional_quotient f.isClosed_ker
+  exact f.toLinearMap.quotKerEquivRange.symm.finiteDimensional
+
+end Compl