diff --git a/Mathlib.lean b/Mathlib.lean
index 2e3a729ae4..638124f210 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -721,6 +721,7 @@ public import Mathlib.Algebra.Lie.Basic
 public import Mathlib.Algebra.Lie.Basis
 public import Mathlib.Algebra.Lie.Basis.Base
 public import Mathlib.Algebra.Lie.Basis.Basic
+public import Mathlib.Algebra.Lie.Basis.Prod
 public import Mathlib.Algebra.Lie.CartanCriterion
 public import Mathlib.Algebra.Lie.CartanExists
 public import Mathlib.Algebra.Lie.CartanSubalgebra
@@ -3578,6 +3579,7 @@ public import Mathlib.Combinatorics.Graph.Basic
 public import Mathlib.Combinatorics.Graph.Delete
 public import Mathlib.Combinatorics.Graph.Lattice
 public import Mathlib.Combinatorics.Graph.Maps
+public import Mathlib.Combinatorics.Graph.Simple
 public import Mathlib.Combinatorics.Graph.Subgraph
 public import Mathlib.Combinatorics.HalesJewett
 public import Mathlib.Combinatorics.Hall.Basic
diff --git a/Mathlib/Algebra/Lie/Basis/Basic.lean b/Mathlib/Algebra/Lie/Basis/Basic.lean
index a9c18c8033..0b0ee9794e 100644
--- a/Mathlib/Algebra/Lie/Basis/Basic.lean
+++ b/Mathlib/Algebra/Lie/Basis/Basic.lean
@@ -5,7 +5,8 @@ Authors: Oliver Nash
 -/
 module
 
-public import Mathlib.Algebra.Lie.Weights.Killing
+public import Mathlib.Algebra.Lie.Sl2
+public import Mathlib.Algebra.Lie.Weights.Cartan
 
 /-!
 # Bases of semisimple Lie algebras
diff --git a/Mathlib/Algebra/Lie/Basis/Prod.lean b/Mathlib/Algebra/Lie/Basis/Prod.lean
new file mode 100644
index 0000000000..70df65bc07
--- /dev/null
+++ b/Mathlib/Algebra/Lie/Basis/Prod.lean
@@ -0,0 +1,309 @@
+/-
+Copyright (c) 2026 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+module
+
+public import Mathlib.Algebra.Lie.Basis.Basic
+public import Mathlib.Algebra.Lie.Prod
+public import Mathlib.Algebra.Lie.Semisimple.Basic
+
+/-!
+# Products of bases Lie algebras
+
+Given two finite-dimensional simple Lie algebras, if they admit bases with matching Cartan matrices,
+they must be isomorphic. This file provides a proof of this as `LieAlgebra.Basis.equivOfReindex`.
+
+-/
+
+noncomputable section
+
+namespace LieAlgebra.Basis
+
+open Function LieSubalgebra Set Submodule
+
+variable {ι₁ ι₂ L₁ L₂ : Type*} [Finite ι₁] [Finite ι₂] (eι : ι₁ ≃ ι₂) [LieRing L₁] [LieRing L₂]
+
+section CommRing
+
+variable {R : Type*} [CommRing R]
+  [LieAlgebra R L₁] {H₁ : LieSubalgebra R L₁} (b₁ : Basis ι₁ H₁)
+  [LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂} (b₂ : Basis ι₂ H₂)
+
+/-- A distinguished subalgebra of the product of two based Lie algebras with equivalent indexing
+sets. -/
+protected def prod :
+    LieSubalgebra R (L₁ × L₂) :=
+  .lieSpan _ _ <|
+    {(b₁.h i, b₂.h (eι i)) | i : ι₁} ∪
+    {(b₁.e i, b₂.e (eι i)) | i : ι₁} ∪
+    {(b₁.f i, b₂.f (eι i)) | i : ι₁}
+
+/-- The equivalence obtained by interchanging the two bases consumed by `LieAlgebra.Basis.prod`. -/
+def prodSymmEquiv : prod eι.symm b₂ b₁ ≃ₗ⁅R⁆ b₁.prod eι b₂ :=
+  have : (prod eι.symm b₂ b₁).map (LieEquiv.prodComm R L₂ L₁) = b₁.prod eι b₂ := by
+    rw [prod, prod, map_lieSpan]; congr; ext; aesop
+  (LieEquiv.lieSubalgebraMap (prod eι.symm b₂ b₁) (LieEquiv.prodComm _ _ _)).trans
+    (LieEquiv.ofEq _ _ <| by simpa)
+
+@[simp]
+lemma prodSymmEquiv_symm_apply {y : b₁.prod eι b₂} :
+    (prodSymmEquiv eι b₁ b₂).symm y =
+      ⟨((y : L₁ × L₂).snd, (y : L₁ × L₂).fst), ((prodSymmEquiv eι b₁ b₂).symm y).property⟩ :=
+  rfl
+
+lemma h_mem_prod (i : ι₁) :
+    (b₁.h i, b₂.h (eι i)) ∈ b₁.prod eι b₂ :=
+  subset_lieSpan <| by aesop
+
+/-- A distinguished subalgebra of the Lie algebra defined by `LieAlgebra.Basis.prod`.
+
+Subject to the assumtions demanded by `LieAlgebra.Basis.isCartanSubalgebra` this will be a Cartan
+subalgebra of `LieAlgebra.Basis.prod`. -/
+def prodCartan :
+    LieSubalgebra R (prod eι b₁ b₂) :=
+  .lieSpan _ _ {⟨(b₁.h i, b₂.h (eι i)), h_mem_prod eι b₁ b₂ i⟩ | i : ι₁}
+
+open Finsupp in
+lemma prodCartanEquiv_aux :
+    InjOn (LinearMap.fst R L₁ L₂) (span R {(b₁.h i, b₂.h (eι i)) | i : ι₁}) := by
+  suffices ∀ y, (∃ l : ι₁ →₀ R,
+      (l.linearCombination R fun i ↦ (b₁.h i, b₂.h (eι i))) = (0, y)) → y = 0 by
+    have aux : {(b₁.h i, b₂.h (eι i)) | i : ι₁} = (fun i : ι₁ ↦ (b₁.h i, b₂.h (eι i))) '' univ := by
+      ext; simp
+    simp_rw [← LinearMap.disjoint_ker_iff_injOn, LinearMap.disjoint_ker, aux,
+      mem_span_image_iff_linearCombination]
+    aesop
+  intro y ⟨f, hf⟩
+  suffices linearCombination R b₁.h f = 0 by
+    rw [LinearMap.map_eq_zero_iff _ b₁.linInd] at this
+    aesop (add simp Prod.ext_iff)
+  replace hf := (LinearMap.fst R L₁ L₂).congr_arg hf
+  rw [← LinearMap.comp_apply, ← Finsupp.linearCombination_linear_comp] at hf
+  aesop
+
+open LinearMap in
+/-- The Lie subalgebra `LieAlgebra.Basis.prod` is a copy of the Cartan subalgebra of the input. -/
+def prodCartanEquiv :
+    prodCartan eι b₁ b₂ ≃ₗ[R] H₁ :=
+  /- Informally this is obvious since `prodCartan eι b₁ b₂` is the linear span of
+  `{(b₁.h i, b₂.h (eι i)) | i : ι₁}` and `H₁` is the linear span of `{b₁.h i | i : ι₁}` (and both
+  families are linearly independent) but formally some care is required. -/
+  have h₁ : (prodCartan eι b₁ b₂).map (prod eι b₁ b₂).incl =
+      (lieSpan R (L₁ × L₂) {(b₁.h i, b₂.h (eι i)) | i : ι₁} : Set (L₁ × L₂)) := by
+    rw [prodCartan, map_lieSpan]; congr; aesop
+  have h₂ : (lieSpan R _ {(b₁.h i, b₂.h (eι i)) | i : ι₁}) =
+      span R {(b₁.h i, b₂.h (eι i)) | i : ι₁} :=
+    coe_lieSpan_eq_span_of_forall_lie_eq_zero <| by simp [b₁.lie_h_h, b₂.lie_h_h]
+  have h₃ : (span R {(b₁.h i, b₂.h (eι i)) | i : ι₁}).map (.fst R L₁ L₂) = span R (range b₁.h) := by
+    rw [Submodule.map_span]; congr; ext; simp
+  have h₄ : lieSpan R L₁ (range b₁.h) = span R (range b₁.h) := by
+    rw [← b₁.coe_cartan_eq_span, toSubmodule_inj, ← b₁.cartan_eq_lieSpan]
+  have h₅ : (H₁ : Set L₁) = lieSpan R L₁ (range b₁.h) := by simp [b₁.cartan_eq_lieSpan]
+  let e₀ : prodCartan eι b₁ b₂ ≃ₗ[R] (prodCartan eι b₁ b₂).map (prod eι b₁ b₂).incl :=
+    (prodCartan eι b₁ b₂).equivMapOfInjective (prod eι b₁ b₂).incl <| by simp
+  let e₁ : (prodCartan eι b₁ b₂).map (prod eι b₁ b₂).incl ≃ₗ[R]
+      lieSpan R (L₁ × L₂) {(b₁.h i, b₂.h (eι i)) | i : ι₁} := LieEquiv.ofEq _ _ h₁
+  let e₂ : lieSpan R (L₁ × L₂) {(b₁.h i, b₂.h (eι i)) | i : ι₁} ≃ₗ[R]
+      span R {(b₁.h i, b₂.h (eι i)) | i : ι₁} := LinearEquiv.ofEq _ _ h₂
+  let e₃ : span R {(b₁.h i, b₂.h (eι i)) | i : ι₁} ≃ₗ[R] span R (range b₁.h) :=
+    (LinearEquiv.ofBijective _ ⟨submoduleMap_injective_of_injOn (prodCartanEquiv_aux eι b₁ b₂),
+      submoduleMap_surjective _ _⟩).trans <| .ofEq _ _ h₃
+  let e₄ : span R (range b₁.h) ≃ₗ[R] lieSpan R L₁ (range b₁.h) := LinearEquiv.ofEq _ _ h₄.symm
+  let e₅ : lieSpan R L₁ (range b₁.h) ≃ₗ[R] H₁ := (LieEquiv.ofEq _ _ h₅).symm
+  e₀.trans <| e₁.trans <| e₂.trans <| e₃.trans <| e₄.trans e₅
+
+protected abbrev prodH (i : ι₁) : b₁.prod eι b₂ :=
+  ⟨(b₁.h i, b₂.h (eι i)), subset_lieSpan <| by aesop⟩
+
+protected abbrev prodE (i : ι₁) : b₁.prod eι b₂ :=
+  ⟨(b₁.e i, b₂.e (eι i)), subset_lieSpan <| by aesop⟩
+
+protected abbrev prodF (i : ι₁) : b₁.prod eι b₂ :=
+  ⟨(b₁.f i, b₂.f (eι i)), subset_lieSpan <| by aesop⟩
+
+lemma basisProd_aux :
+    lieSpan R (prod eι b₁ b₂) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) = ⊤ := by
+  suffices lieSpan R (prod eι b₁ b₂) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
+      lieSpan R (prod eι b₁ b₂)
+        (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) by
+    have hr : range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) =
+        Subtype.val ⁻¹' ( {(b₁.h i, b₂.h (eι i)) | i : ι₁} ∪
+                          {(b₁.e i, b₂.e (eι i)) | i : ι₁} ∪
+                          {(b₁.f i, b₂.f (eι i)) | i : ι₁} ) := by
+      ext; simp [Subtype.ext_iff]
+    rw [this, hr]
+    exact lieSpan_lieSpan_coe_preimage
+  simp only [union_assoc]
+  refine le_antisymm (lieSpan_mono <| by simp) (lieSpan_le.mpr <| union_subset ?_ subset_lieSpan)
+  rintro - ⟨i, rfl⟩
+  have hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆ := by
+    simp [Subtype.ext_iff, (b₁.sl2 i).lie_e_f, (b₂.sl2 (eι i)).lie_e_f]
+  rw [hef]
+  apply lie_mem
+  · exact subset_lieSpan <| mem_union_left _ <| mem_range_self i
+  · exact subset_lieSpan <| mem_union_right _ <| mem_range_self i
+
+/-- A distinguished basis carried by `LieAlgebra.Basis.prod`. -/
+def basisProd (hA : b₁.A.reindex eι eι = b₂.A) :
+    Basis ι₁ (prodCartan eι b₁ b₂) where
+  A := b₁.A
+  h := prodH eι b₁ b₂
+  e := prodE eι b₁ b₂
+  f := prodF eι b₁ b₂
+  cartan_eq_lieSpan := rfl
+  span_ef := b₁.basisProd_aux eι b₂
+  linInd := .of_comp (prod eι b₁ b₂).subtype <| .of_comp (LinearMap.fst R L₁ L₂) b₁.linInd
+  nondegen := b₁.nondegen
+  sl2 i :=
+    { h_ne_zero := by simp [Subtype.ext_iff, (b₁.sl2 i).h_ne_zero]
+      lie_e_f := by simp [Subtype.ext_iff, (b₁.sl2 i).lie_e_f, (b₂.sl2 (eι i)).lie_e_f]
+      lie_h_e_nsmul := by
+        simp [Subtype.ext_iff, (b₁.sl2 i).lie_h_e_nsmul, (b₂.sl2 (eι i)).lie_h_e_nsmul]
+      lie_h_f_nsmul := by
+        simp [Subtype.ext_iff, (b₁.sl2 i).lie_h_f_nsmul, (b₂.sl2 (eι i)).lie_h_f_nsmul] }
+  lie_h_h i j := by simp [Subtype.ext_iff, b₁.lie_h_h, b₂.lie_h_h]
+  lie_h_e i j := by simp [Subtype.ext_iff, b₁.lie_h_e, b₂.lie_h_e, ← hA]
+  lie_h_f i j := by simp [Subtype.ext_iff, b₁.lie_h_f, b₂.lie_h_f, ← hA]
+  lie_e_f_ne i j hij := by
+    have hij' : eι i ≠ eι j := by aesop
+    simp [Subtype.ext_iff, b₁.lie_e_f_ne i j hij, b₂.lie_e_f_ne _ _ hij']
+
+lemma surjective_fst_prod :
+    Surjective ((LieHom.fst R L₁ L₂).comp (prod eι b₁ b₂).incl) := by
+  set L : LieSubalgebra R (L₁ × L₂) := b₁.prod eι b₂
+  set p₁ : L →ₗ⁅R⁆ L₁ := (LieHom.fst R L₁ L₂).comp L.incl
+  have h₁ : range b₁.e = range (p₁ ∘ prodE eι b₁ b₂) := rfl
+  have h₂ : range b₁.f = range (p₁ ∘ prodF eι b₁ b₂) := rfl
+  rw [← LieHom.range_eq_top, eq_top_iff, ← b₁.span_ef, map_top, ← b₁.basisProd_aux eι b₂,
+    map_lieSpan, image_union, h₁, h₂]
+  simp [range_comp]
+
+lemma surjective_snd_prod :
+    Surjective ((LieHom.snd R L₁ L₂).comp (prod eι b₁ b₂).incl) := by
+  set L : LieSubalgebra R (L₁ × L₂) := b₁.prod eι b₂
+  set p₂ : L →ₗ⁅R⁆ L₂ := (LieHom.snd R L₁ L₂).comp L.incl
+  have h₁ : range b₂.e = range (p₂ ∘ prodE eι b₁ b₂) := by
+    simp [show p₂ ∘ prodE eι b₁ b₂ = b₂.e ∘ eι from rfl]
+  have h₂ : range b₂.f = range (p₂ ∘ prodF eι b₁ b₂) := by
+    simp [show p₂ ∘ prodF eι b₁ b₂ = b₂.f ∘ eι from rfl]
+  rw [← LieHom.range_eq_top, eq_top_iff, ← b₂.span_ef, map_top,
+    ← b₁.basisProd_aux eι b₂, map_lieSpan, image_union, h₁, h₂]
+  simp [range_comp]
+
+lemma lie_fst_eq_zero_of_mem_prodCartan
+    {y : b₁.prod eι b₂} (hy : y ∈ prodCartan eι b₁ b₂) (x : H₁) :
+    ⁅(y : L₁ × L₂).fst, (x : L₁)⁆ = 0 := by
+  have := b₁.isLieAbelian_cartan
+  induction hy using lieSpan_induction with
+  | mem u hu =>
+    obtain ⟨i, rfl⟩ := hu
+    suffices ⁅b₁.h' i, x⁆ = 0 by simpa [Subtype.ext_iff, Basis.h'] using this
+    apply trivial_lie_zero
+  | zero => simp
+  | add u v hu hv hu' hv' => simp [hu', hv']
+  | smul t u hu hu' => simp [hu']
+  | lie u v hu hv hu' hv' => simp [hu', hv']
+
+lemma lie_snd_eq_zero_of_mem_prodCartan
+    {y : b₁.prod eι b₂} (hy : y ∈ prodCartan eι b₁ b₂) (x : H₂) :
+    ⁅(y : L₁ × L₂).snd, (x : L₂)⁆ = 0 := by
+  suffices (prodSymmEquiv eι b₁ b₂).symm y ∈ prodCartan eι.symm b₂ b₁ from
+    lie_fst_eq_zero_of_mem_prodCartan eι.symm b₂ b₁ this x
+  replace hy :
+      (prodSymmEquiv eι b₁ b₂).symm y ∈ (prodCartan eι b₁ b₂).map (prodSymmEquiv eι b₁ b₂).symm :=
+    mem_image_of_mem (prodSymmEquiv eι b₁ b₂).symm hy
+  rw [prodCartan, map_lieSpan] at hy
+  rw [prodCartan]
+  convert hy
+  ext; simp; grind
+
+end CommRing
+
+section Field
+
+variable {K : Type*} [Field K] [CharZero K]
+  [LieAlgebra K L₁] [FiniteDimensional K L₁] {H₁ : LieSubalgebra K L₁} (b₁ : Basis ι₁ H₁)
+  [LieAlgebra K L₂] [FiniteDimensional K L₂] {H₂ : LieSubalgebra K L₂} (b₂ : Basis ι₂ H₂)
+  (hA : b₁.A.reindex eι eι = b₂.A)
+include hA
+
+lemma prod_lt_top [Nontrivial L₂] :
+    b₁.prod eι b₂ < ⊤ := by
+  /- This innocent-looking result is the key. The informal literature seems only to contain
+  somewhat heavy-weight proofs (e.g., [Chapter IV, Theorem 14.2](humphreys1972) makes an
+  inductive argument using highest weights) but in fact it follows very easily from
+  `LieAlgebra.Basis.isCartanSubalgebra`. The argument is essentially: if `b₁.prod eι b₂` is not
+  proper then it's Cartan subalgebra contains `H₁ × H₂` which is absurd since it
+  `LieAlgebra.Basis.prodCartanEquiv` tells us it is equivalent to `H₁`. -/
+  have := Fintype.ofFinite ι₁
+  have := Fintype.ofFinite ι₂
+  have := b₁.isCartanSubalgebra
+  have := b₂.isCartanSubalgebra
+  have := (basisProd eι b₁ b₂ hA).isCartanSubalgebra
+  rw [lt_top_iff_ne_top]
+  intro contra
+  have (x : H₁ × H₂) (hx) : ⟨(x.1, x.2), hx⟩ ∈ prodCartan eι b₁ b₂ := by
+    rw [← mem_toLieSubmodule, ← rootSpace_zero_eq, LieModule.mem_genWeightSpace]
+    refine fun ⟨y, hy⟩ ↦ ⟨1, ?_⟩
+    simpa [Subtype.ext_iff] using ⟨lie_fst_eq_zero_of_mem_prodCartan eι b₁ b₂ hy x.fst,
+      lie_snd_eq_zero_of_mem_prodCartan eι b₁ b₂ hy x.snd⟩
+  let f : H₁ × H₂ →ₗ[K] prodCartan eι b₁ b₂ :=
+    { toFun x := ⟨⟨⟨x.fst, x.snd⟩, by simp [contra]⟩, this x _⟩
+      map_add' := by simp
+      map_smul' := by simp }
+  have f_inj : Injective f := fun x y h ↦ by simpa [Prod.ext_iff, f] using h
+  let g : H₁ × H₂ →ₗ[K] H₁ := (prodCartanEquiv eι b₁ b₂) ∘ₗ f
+  have hg₁ : Injective g := by simpa [g]
+  obtain ⟨x₂ : H₂, hx₂ : x₂ ≠ 0⟩ := exists_ne (0 : H₂)
+  have hg₂ : g (0, x₂) = g (0, 0) := rfl
+  aesop
+
+variable [IsSimple K L₁] [IsSimple K L₂]
+
+/-- `LieAlgebra.Basis.prod` is equivalent to its left input algebra. -/
+def prodEquivLeft :
+    b₁.prod eι b₂ ≃ₗ⁅K⁆ L₁ :=
+  let L : LieSubalgebra K (L₁ × L₂) := b₁.prod eι b₂
+  let p₁ : L →ₗ⁅K⁆ L₁ := (LieHom.fst K L₁ L₂).comp L.incl
+  have : Injective p₁ := by
+    let p₂ : L →ₗ⁅K⁆ L₂ := (LieHom.snd K L₁ L₂).comp L.incl
+    have disj : Disjoint p₁.ker p₂.ker := by
+      rw [disjoint_iff, _root_.eq_bot_iff]
+      rintro ⟨⟨x, y⟩, -⟩
+      simp [p₁, p₂, Subtype.ext_iff]
+    set I₁ : LieIdeal K L₂ := p₁.ker.map p₂
+    suffices I₁ ≠ ⊤ by
+      replace this := (IsSimple.eq_bot_or_eq_top I₁).resolve_right this
+      rw [LieIdeal.map_eq_bot_iff] at this
+      rw [← p₁.ker_eq_bot, disj.eq_bot_of_le this]
+    have : Nontrivial L₂ := IsSimple.nontrivial K L₂
+    have := (prod_lt_top eι b₁ b₂ hA).ne
+    contrapose this
+    have hI₁ : (I₁ : Set L₂) = p₂ '' p₁.ker :=
+      congr_arg SetLike.coe <| p₁.ker.coe_map_of_surjective (surjective_snd_prod eι b₁ b₂)
+    have hL₂ (x₂ : L₂) : (0, x₂) ∈ L := by
+      replace this : x₂ ∈ (I₁ : Set L₂) := by simp [this]
+      simpa [p₂, p₁, hI₁] using this
+    have hL₁ (x₁ : L₁) : (x₁, 0) ∈ L := by
+      obtain ⟨⟨⟨-, y⟩, hy⟩, rfl⟩ : x₁ ∈ range p₁ := mem_range.mpr (surjective_fst_prod eι b₁ b₂ x₁)
+      simpa [p₁] using sub_mem hy (hL₂ y)
+    rw [eq_top_iff]
+    rintro ⟨x₁, x₂⟩ -
+    simpa using add_mem (hL₁ x₁) (hL₂ x₂)
+  .ofBijective p₁ ⟨this, surjective_fst_prod eι b₁ b₂⟩
+
+/-- `LieAlgebra.Basis.prod` is equivalent to its right input algebra. -/
+def prodEquivRight :
+    b₁.prod eι b₂ ≃ₗ⁅K⁆ L₂ :=
+  (prodSymmEquiv eι b₁ b₂).symm.trans (prodEquivLeft eι.symm b₂ b₁ <| by simp [← hA])
+
+/-- Simple Lie algebras with equivalent bases are equivalent. -/
+public def equivOfReindex :
+    L₁ ≃ₗ⁅K⁆ L₂ :=
+  (prodEquivLeft eι b₁ b₂ hA).symm.trans (prodEquivRight eι b₁ b₂ hA)
+
+end Field
+
+end LieAlgebra.Basis
diff --git a/Mathlib/Algebra/Lie/Prod.lean b/Mathlib/Algebra/Lie/Prod.lean
index ad29ba43b0..d7c96694a6 100644
--- a/Mathlib/Algebra/Lie/Prod.lean
+++ b/Mathlib/Algebra/Lie/Prod.lean
@@ -209,4 +209,10 @@ theorem prodMap_zero : (0 : L₁ →ₗ⁅R⁆ L₃).prodMap (0 : L₂ →ₗ⁅
 
 end LieHom
 
+variable (R L₁ L₂) in
+/-- The map `(x, y) ↦ (y, x)` as a Lie equivalence. -/
+@[simps!] def LieEquiv.prodComm : (L₁ × L₂) ≃ₗ⁅R⁆ L₂ × L₁ where
+  __ := LinearEquiv.prodComm R L₁ L₂
+  map_lie' := by simp
+
 end
diff --git a/Mathlib/Algebra/Lie/Semisimple/Basic.lean b/Mathlib/Algebra/Lie/Semisimple/Basic.lean
index 85a7ece212..8775195af3 100644
--- a/Mathlib/Algebra/Lie/Semisimple/Basic.lean
+++ b/Mathlib/Algebra/Lie/Semisimple/Basic.lean
@@ -87,6 +87,13 @@ instance : LieModule.IsIrreducible R L L := by
   contrapose _i
   infer_instance
 
+include R in
+/-- A simple lie algebra is non-trivial. -/
+lemma nontrivial : Nontrivial L := by
+  have := IsSimple.non_abelian R (L := L)
+  contrapose! this
+  infer_instance
+
 protected lemma isAtom_top : IsAtom (⊤ : LieIdeal R L) := isAtom_top
 
 variable {R L} in
diff --git a/Mathlib/Algebra/Lie/Subalgebra.lean b/Mathlib/Algebra/Lie/Subalgebra.lean
index c7c82acb21..08df1c027d 100644
--- a/Mathlib/Algebra/Lie/Subalgebra.lean
+++ b/Mathlib/Algebra/Lie/Subalgebra.lean
@@ -376,6 +376,15 @@ def comap : LieSubalgebra R L :=
 
 @[simp] lemma mem_comap {x : L} : x ∈ K₂.comap f ↔ f x ∈ K₂ := Iff.rfl
 
+/-- A Lie subalgebra is equivalent to its push forward along an injective linear map. -/
+@[simps!] noncomputable def equivMapOfInjective (hf : Function.Injective f) :
+    K ≃ₗ⁅R⁆ K.map f where
+  __ := Submodule.equivMapOfInjective f.toLinearMap hf K
+  map_lie' {x y} := by
+    ext
+    change f ⁅(x : L), (y : L)⁆ = ⁅f (x : L), f (y : L)⁆
+    simp
+
 section LatticeStructure
 
 open Set
@@ -542,6 +551,8 @@ variable (R L)
 instance wellFoundedGT_of_noetherian [IsNoetherian R L] : WellFoundedGT (LieSubalgebra R L) :=
   RelHomClass.isWellFounded (⟨toSubmodule, @fun _ _ h ↦ h⟩ : _ →r (· > ·))
 
+theorem map_top : f.range = LieSubalgebra.map f ⊤ := by ext; simp
+
 variable {R L K K' f}
 
 section NestedSubalgebras
@@ -670,6 +681,13 @@ theorem coe_lieSpan_eq_span_of_forall_lie_eq_zero
   | smul_left r x y _ _ h => simp [smul_mem _ r h]
   | smul_right r x y _ _ h => simp [smul_mem _ r h]
 
+theorem map_lieSpan :
+    (lieSpan R L s).map f = lieSpan R L₂ (f '' s) := by
+  refine le_antisymm ?_ (lieSpan_le.mpr <| Set.image_mono subset_lieSpan)
+  rw [map_le_iff_le_comap, lieSpan_le]
+  change s ⊆ f ⁻¹' (lieSpan R L₂ (f '' s))
+  exact image_subset_iff.mp <| subset_lieSpan
+
 variable (R L)
 
 /-- `lieSpan` forms a Galois insertion with the coercion from `LieSubalgebra` to `Set`. -/
diff --git a/Mathlib/Algebra/Module/Submodule/Ker.lean b/Mathlib/Algebra/Module/Submodule/Ker.lean
index edc703d483..37a58fe84b 100644
--- a/Mathlib/Algebra/Module/Submodule/Ker.lean
+++ b/Mathlib/Algebra/Module/Submodule/Ker.lean
@@ -164,6 +164,11 @@ def iterateKer (f : M →ₗ[R] M) : ℕ →o Submodule R M where
     rw [LinearMap.mem_ker] at h
     rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, map_zero]
 
+lemma ker_submoduleMap {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁]
+    (f : M →ₛₗ[τ₁₂] M₂) (p : Submodule R M) :
+    (f.submoduleMap p).ker = f.ker.comap p.subtype := by
+  ext; simp [Subtype.ext_iff]
+
 end AddCommMonoid
 
 section Ring
diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean
index 87b6047a2a..bb3e5df6eb 100644
--- a/Mathlib/Algebra/Module/Submodule/Map.lean
+++ b/Mathlib/Algebra/Module/Submodule/Map.lean
@@ -675,6 +675,13 @@ theorem submoduleMap_injective [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ
     (p : Submodule R M) : Injective (f.submoduleMap p) :=
   f.toAddMonoidHom.addSubmonoidMap_injective hf _
 
+theorem submoduleMap_injective_of_injOn [RingHomSurjective σ₁₂]
+    {p : Submodule R M} {f : M →ₛₗ[σ₁₂] M₂} (hf : Set.InjOn f p) :
+    Injective (f.submoduleMap p) := by
+  intro ⟨x, hx⟩ ⟨y, hy⟩ hxy
+  replace hxy : f x = f y := by simpa [Subtype.ext_iff] using hxy
+  aesop
+
 open Submodule
 
 theorem map_codRestrict [RingHomSurjective σ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h p') :
diff --git a/Mathlib/Algebra/MonoidAlgebra/Basic.lean b/Mathlib/Algebra/MonoidAlgebra/Basic.lean
index 57fa8f1f92..23fc281e99 100644
--- a/Mathlib/Algebra/MonoidAlgebra/Basic.lean
+++ b/Mathlib/Algebra/MonoidAlgebra/Basic.lean
@@ -684,20 +684,36 @@ end AddMonoidAlgebra
 
 variable [CommSemiring R] [Semiring A] [Algebra R A]
 
-set_option backward.isDefEq.respectTransparency false in
-variable (A M) in
+namespace AddMonoidAlgebra
+variable [AddMonoid M]
+
+variable (R A M) in
 /-- The algebra equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
 `Multiplicative`. -/
-def AddMonoidAlgebra.toMultiplicativeAlgEquiv [AddMonoid M] :
-    AddMonoidAlgebra A M ≃ₐ[R] MonoidAlgebra A (Multiplicative M) where
-  toRingEquiv := AddMonoidAlgebra.toMultiplicative A M
-  commutes' r := by simp [AddMonoidAlgebra.toMultiplicative]
+@[simps!]
+def toMultiplicativeAlgEquiv : AddMonoidAlgebra A M ≃ₐ[R] MonoidAlgebra A (Multiplicative M) where
+  toRingEquiv := toMultiplicative A M
+  commutes' r := by ext; simp
 
-set_option backward.isDefEq.respectTransparency false in
-variable (A M) in
+@[simp]
+lemma toMultiplicativeAlgEquiv_single (m : M) (a : A) :
+    toMultiplicativeAlgEquiv R A M (single m a) = .single (.ofAdd m) a := by ext; simp
+
+end AddMonoidAlgebra
+
+namespace MonoidAlgebra
+variable [Monoid M]
+
+variable (R A M) in
 /-- The algebra equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of
 `Additive`. -/
-def MonoidAlgebra.toAdditiveAlgEquiv [Monoid M] :
-    MonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra A (Additive M) where
-  toRingEquiv := MonoidAlgebra.toAdditive A M
-  commutes' r := by simp [MonoidAlgebra.toAdditive]
+@[simps!]
+def toAdditiveAlgEquiv : MonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra A (Additive M) where
+  toRingEquiv := toAdditive A M
+  commutes' r := by simp [toAdditive]
+
+@[simp]
+lemma toAdditiveAlgEquiv_single (m : M) (a : A) :
+    toAdditiveAlgEquiv R A M (single m a) = .single (.ofMul m) a := by ext; simp
+
+end MonoidAlgebra
diff --git a/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean b/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean
index 6ae7e4da44..36186ecbe9 100644
--- a/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean
+++ b/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean
@@ -486,12 +486,15 @@ end MonoidAlgebra
 #### Conversions between `AddMonoidAlgebra` and `MonoidAlgebra`
 -/
 
+namespace AddMonoidAlgebra
+variable [Semiring R] [Add M]
+
 set_option backward.isDefEq.respectTransparency false in
-variable (k G) in
+variable (R M) in
 /-- The equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
 `Multiplicative` -/
-protected def AddMonoidAlgebra.toMultiplicative [Semiring k] [Add G] :
-    AddMonoidAlgebra k G ≃+* MonoidAlgebra k (Multiplicative G) where
+@[simps]
+def toMultiplicative : AddMonoidAlgebra R M ≃+* MonoidAlgebra R (Multiplicative M) where
   toFun x := .ofCoeff <| x.coeff.mapDomain .ofAdd
   invFun x := .ofCoeff <| x.coeff.mapDomain Multiplicative.toAdd
   left_inv x := by ext; simp
@@ -500,14 +503,23 @@ protected def AddMonoidAlgebra.toMultiplicative [Semiring k] [Add G] :
   map_mul' x y := by
     classical
     ext
-    simp [MonoidAlgebra.coeff_mul, AddMonoidAlgebra.coeff_mul, Finsupp.sum_mapDomain_index, add_mul,
-      mul_add, ite_add_zero, Multiplicative.ext_iff]
+    simp [MonoidAlgebra.coeff_mul, coeff_mul, sum_mapDomain_index, add_mul, mul_add, ite_add_zero,
+      Multiplicative.ext_iff]
+
+@[simp]
+lemma toMultiplicative_single (m : M) (r : R) :
+    toMultiplicative R M (single m r) = .single (.ofAdd m) r := by simp [toMultiplicative]
+
+end AddMonoidAlgebra
+
+namespace MonoidAlgebra
+variable [Semiring R] [Mul M]
 
 set_option backward.isDefEq.respectTransparency false in
-variable (k G) in
+variable (R M) in
 /-- The equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of `Additive` -/
-protected def MonoidAlgebra.toAdditive [Semiring k] [Mul G] :
-    MonoidAlgebra k G ≃+* AddMonoidAlgebra k (Additive G) where
+@[simps]
+def toAdditive : MonoidAlgebra R M ≃+* AddMonoidAlgebra R (Additive M) where
   toFun x := .ofCoeff <| x.coeff.mapDomain .ofMul
   invFun x := .ofCoeff <| x.coeff.mapDomain Additive.toMul
   left_inv x := by ext; simp
@@ -516,5 +528,11 @@ protected def MonoidAlgebra.toAdditive [Semiring k] [Mul G] :
   map_mul' x y := by
     classical
     ext
-    simp [MonoidAlgebra.coeff_mul, AddMonoidAlgebra.coeff_mul, Finsupp.sum_mapDomain_index, add_mul,
-      mul_add, ite_add_zero, Additive.ext_iff]
+    simp [coeff_mul, AddMonoidAlgebra.coeff_mul, sum_mapDomain_index, add_mul, mul_add,
+      ite_add_zero, Additive.ext_iff]
+
+@[simp]
+lemma toAdditive_single (m : M) (r : R) : toAdditive R M (single m r) = .single (.ofMul m) r := by
+  ext; simp
+
+end MonoidAlgebra
diff --git a/Mathlib/Combinatorics/Graph/Simple.lean b/Mathlib/Combinatorics/Graph/Simple.lean
new file mode 100644
index 0000000000..008686765f
--- /dev/null
+++ b/Mathlib/Combinatorics/Graph/Simple.lean
@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Jun Kwon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jun Kwon, Peter Nelson
+-/
+module
+
+public import Mathlib.Combinatorics.Graph.Subgraph
+public import Mathlib.Combinatorics.SimpleGraph.Maps
+
+/-!
+# Simple graphs
+
+This file defines two type classes for graphs `Graph α β`: `Loopless` and `Simple`.
+
+## Main definitions
+- `Loopless`: a graph is loopless if it has no loops
+- `Simple`: a graph is simple if it has no multiple edges between the same pair of vertices
+- `toSimpleGraph`: a function that constructs a `SimpleGraph V(G)` from a Graph `G`
+- `ofSimpleGraph`: a function that constructs a `Graph α (Sym2 α)` from a `SimpleGraph α`
+
+TODO: Show `ofSimpleGraph (toSimpleGraph G)` is isomorphic to `G` when isomorphism on `Graph` is
+defined.
+-/
+
+public section
+
+variable {α β : Type*} {G H : Graph α β} {u v : α} {e f : β} {X Y : Set α}
+
+open Set SimpleGraph
+
+namespace Graph
+
+section Loopless
+
+/-- A loopless graph is one where the ends of every edge are distinct. -/
+@[mk_iff]
+protected class Loopless (G : Graph α β) : Prop where
+  not_isLoopAt : ∀ e x, ¬ G.IsLoopAt e x
+
+@[simp]
+lemma not_isLoopAt (G : Graph α β) [G.Loopless] (e : β) (x : α) : ¬ G.IsLoopAt e x :=
+  Loopless.not_isLoopAt e x
+
+lemma not_adj_self (G : Graph α β) [G.Loopless] (x : α) : ¬ G.Adj x x :=
+  fun ⟨e, he⟩ ↦ Loopless.not_isLoopAt e x he
+
+lemma Adj.ne [G.Loopless] (hxy : G.Adj u v) : u ≠ v := fun h ↦ G.not_adj_self u <| h ▸ hxy
+
+lemma IsLink.ne [G.Loopless] (he : G.IsLink e u v) : u ≠ v := Adj.ne ⟨e, he⟩
+
+lemma loopless_iff_forall_ne_of_adj : G.Loopless ↔ ∀ u v, G.Adj u v → u ≠ v :=
+  ⟨fun _ _ _ h ↦ h.ne, fun h ↦ ⟨fun _ x hex ↦ h x x hex.adj rfl⟩⟩
+
+lemma vertexSet_nontrivial_of_edgeSet_nonempty_of_loopless [G.Loopless] (hE : E(G).Nonempty) :
+    V(G).Nontrivial := by
+  obtain ⟨e, he⟩ := hE
+  obtain ⟨x, y, hxy⟩ := exists_isLink_of_mem_edgeSet he
+  exact ⟨x, hxy.left_mem, y, hxy.right_mem, hxy.adj.ne⟩
+
+lemma Loopless.anti [hG : G.Loopless] (hle : H ≤ G) : H.Loopless := by
+  rw [loopless_iff_forall_ne_of_adj] at hG ⊢
+  exact fun x y hxy ↦ hG x y <| hxy.mono hle
+
+@[simp]
+lemma Inc.isNonloopAt [G.Loopless] (h : G.Inc e u) : G.IsNonloopAt e u :=
+  h.isLoopAt_or_isNonloopAt.resolve_left (Loopless.not_isLoopAt _ _)
+
+end Loopless
+
+section Simple
+
+/-- A `Simple` graph is a `Loopless` graph where no pair of vertices are the ends of more than one
+edge. -/
+@[mk_iff]
+class Simple (G : Graph α β) : Prop extends G.Loopless where
+  eq_of_isLink : ∀ ⦃e f x y⦄, G.IsLink e x y → G.IsLink f x y → e = f
+
+variable [G.Simple]
+
+lemma IsLink.eq (h : G.IsLink e u v) (h' : G.IsLink f u v) : e = f :=
+  Simple.eq_of_isLink h h'
+
+lemma Simple.anti (hle : H ≤ G) : H.Simple where
+  not_isLoopAt e x := by simp [toLoopless.anti hle]
+  eq_of_isLink e f x y he hf := (he.mono hle).eq (hf.mono hle)
+
+instance (V : Set α) : (Graph.noEdge V β).Simple where
+  not_isLoopAt := by simp [IsLoopAt]
+  eq_of_isLink := by simp
+
+instance : (⊥ : Graph α β).Simple := inferInstanceAs (Graph.noEdge _ β).Simple
+
+end Simple
+
+section toSimpleGraph
+
+/-- Construct a simple graph from a graph. -/
+@[expose, simps (attr := grind =)]
+def toSimpleGraph (G : Graph α β) : SimpleGraph V(G) where
+  Adj u v := u ≠ v ∧ G.Adj u v
+  symm := ⟨fun u v ↦ by grind [adj_comm]⟩
+
+lemma toSimpleGraph_adj_iff [G.Loopless] (u v : V(G)) : G.toSimpleGraph.Adj u v ↔ G.Adj u v := by
+  grind [Adj.ne]
+
+lemma toSimpleGraph_mono (h : G ≤s H) : G.toSimpleGraph ≤ h.vertexSet_eq ▸ H.toSimpleGraph := by
+  rintro u v hadj
+  match G, H with
+  | ⟨GV, GL, GE, _, _, _, _⟩, ⟨HV, HL, HE, _, _, _, _⟩ =>
+    obtain ⟨hne, hadj⟩ := toSimpleGraph_adj .. ▸ hadj
+    obtain ⟨hle, h⟩ := h
+    simp only at h
+    subst GV
+    simp [toSimpleGraph_adj, hne, hadj.mono hle]
+
+/-- Construct a graph from a simple graph. It has every element of the vertex type as a vertex. -/
+@[expose, simps (attr := grind =)]
+def ofSimpleGraph (G : SimpleGraph α) : Graph α (Sym2 α) where
+  vertexSet := Set.univ
+  edgeSet := G.edgeSet
+  IsLink e x y := e = s(x, y) ∧ e ∈ G.edgeSet
+  isLink_symm e he := ⟨fun u v ↦ by simp [Sym2.eq_swap]⟩
+  eq_or_eq_of_isLink_of_isLink e u v x y he hf := by grind
+  edge_mem_iff_exists_isLink e := by induction e with | h u v => grind
+
+@[simp]
+lemma ofSimpleGraph_adj_iff {G : SimpleGraph α} (u v : α) :
+    (ofSimpleGraph G).Adj u v ↔ G.Adj u v := by simp [Adj]
+
+/-- The isomorphism between `toSimpleGraph (ofSimpleGraph G)` and `G`. -/
+def toSimpleGraphOfSimpleGraphIso (G : SimpleGraph α) :
+    (toSimpleGraph (ofSimpleGraph G)) ≃g G := by
+  use Equiv.Set.univ α
+  refine ⟨fun h ↦ ⟨fun h' ↦ h.ne (congrArg Subtype.val h'), ?_⟩, fun ⟨_, h⟩ ↦ ?_⟩ <;>
+    revert h <;> rw [ofSimpleGraph_adj_iff] <;> exact id
+
+end toSimpleGraph
+
+end Graph
diff --git a/Mathlib/Order/CompleteLattice/Basic.lean b/Mathlib/Order/CompleteLattice/Basic.lean
index 9ac1a9e45d..41b80c78b1 100644
--- a/Mathlib/Order/CompleteLattice/Basic.lean
+++ b/Mathlib/Order/CompleteLattice/Basic.lean
@@ -441,18 +441,11 @@ theorem iSup₂_comm {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι
 
 @[to_dual (attr := simp)]
 theorem iSup_iSup_eq_left {b : β} {f : ∀ x : β, x = b → α} : ⨆ x, ⨆ h : x = b, f x h = f b rfl :=
-  (le_iSup₂ (f := f) b rfl).antisymm'
-    (iSup_le fun c =>
-      iSup_le <| by
-        rintro rfl
-        rfl)
+  le_antisymm (iSup₂_le fun _ h ↦ h ▸ le_rfl) (le_iSup₂ (f := f) b rfl)
 
 @[to_dual (attr := simp)]
 theorem iSup_iSup_eq_right {b : β} {f : ∀ x : β, b = x → α} : ⨆ x, ⨆ h : b = x, f x h = f b rfl :=
-  (le_iSup₂ b rfl).antisymm'
-    (iSup₂_le fun c => by
-      rintro rfl
-      rfl)
+  le_antisymm (iSup₂_le fun _ h ↦ h ▸ le_refl (f b rfl)) (le_iSup₂ b rfl)
 
 @[to_dual]
 theorem iSup_subtype {p : ι → Prop} {f : Subtype p → α} : iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ :=
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
index 9767efeee0..c3f5582bb7 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
@@ -380,6 +380,26 @@ lemma ciInf_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α
     ⨅ i ∈ (f '' s), g i = ⨅ x ∈ s, g (f x) :=
   ciSup_image (α := αᵒᵈ) hf hg'
 
+theorem le_ciSup_ciSup_eq_left {b : β} {f : ∀ x : β, x = b → α} :
+    f b rfl ≤ ⨆ x, ⨆ h : x = b, f x h := by
+  refine le_ciSup₂ (f := f) ⟨f b rfl, ?_⟩ b rfl
+  rintro a ⟨_, ⟨b, rfl⟩, ⟨rfl, rfl⟩⟩
+  rfl
+
+theorem ciInf_ciInf_eq_left_le {b : β} {f : ∀ x : β, x = b → α} :
+    ⨅ x, ⨅ h : x = b, f x h ≤ f b rfl :=
+  le_ciSup_ciSup_eq_left (α := αᵒᵈ)
+
+theorem le_ciSup_ciSup_eq_right {b : β} {f : ∀ x : β, b = x → α} :
+    f b rfl ≤ ⨆ x, ⨆ h : b = x, f x h := by
+  refine le_ciSup₂ ⟨f b rfl, ?_⟩ b rfl
+  rintro a ⟨_, ⟨b, rfl⟩, ⟨rfl, rfl⟩⟩
+  rfl
+
+theorem ciInf_ciInf_eq_right_le {b : β} {f : ∀ x : β, b = x → α} :
+    ⨅ x, ⨅ h : b = x, f x h ≤ f b rfl :=
+  le_ciSup_ciSup_eq_right (α := αᵒᵈ)
+
 /-- Note that equality need not hold: consider `ι := Bool, p := (·), α := ℤ, f := fun _ ↦ -1`,
 then the LHS is `-1` but the RHS is `-1 ⊔ sSup ∅ = -1 ⊔ 0 = 0`. -/
 theorem ciSup_exists_le {p : ι → Prop} {f : Exists p → α} : ⨆ ih, f ih ≤ ⨆ (i) (h), f ⟨i, h⟩ := by
@@ -553,6 +573,16 @@ theorem ciSup_exists {p : ι → Prop} {f : Exists p → α} : ⨆ ih, f ih = 
   refine le_antisymm ciSup_exists_le <| ciSup_le' fun i ↦ ciSup_le' fun hi ↦ ?_
   simp [show Exists p from ⟨i, hi⟩]
 
+@[simp]
+theorem ciSup_ciSup_eq_left {b : β} {f : ∀ x : β, x = b → α} :
+    ⨆ x, ⨆ h : x = b, f x h = f b rfl :=
+  le_antisymm (ciSup_le' fun _ ↦ ciSup_le' (· ▸ le_rfl)) le_ciSup_ciSup_eq_left
+
+@[simp]
+theorem ciSup_ciSup_eq_right {b : β} {f : ∀ x : β, b = x → α} :
+    ⨆ x, ⨆ h : b = x, f x h = f b rfl :=
+  le_antisymm (ciSup_le' fun _ ↦ ciSup_le' (· ▸ le_refl (f b rfl))) le_ciSup_ciSup_eq_right
+
 lemma ciSup_or' (p q : Prop) (f : p ∨ q → α) :
     ⨆ (h : p ∨ q), f h = (⨆ h : p, f (.inl h)) ⊔ ⨆ h : q, f (.inr h) := by
   by_cases hp : p <;>
diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean
index 72e3d37a65..0e98b27261 100644
--- a/Mathlib/Probability/Process/Stopping.lean
+++ b/Mathlib/Probability/Process/Stopping.lean
@@ -442,7 +442,7 @@ variable [Preorder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι}
 /-- The associated σ-algebra with a stopping time. -/
 @[instance_reducible]
 protected def measurableSpace (hτ : IsStoppingTime f τ) : MeasurableSpace Ω where
-  MeasurableSet' s := MeasurableSet s ∧ ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i})
+  MeasurableSet' s := MeasurableSet[⨆ t, f t] s ∧ ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i})
   measurableSet_empty := by simp
   measurableSet_compl s hs := by
     refine ⟨hs.1.compl, fun i ↦ ?_⟩
@@ -462,7 +462,7 @@ protected def measurableSpace (hτ : IsStoppingTime f τ) : MeasurableSpace Ω w
 
 protected theorem measurableSet (hτ : IsStoppingTime f τ) (s : Set Ω) :
     MeasurableSet[hτ.measurableSpace] s
-      ↔ MeasurableSet s ∧ ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) :=
+      ↔ MeasurableSet[⨆ t, f t] s ∧ ∀ i : ι, MeasurableSet[f i] (s ∩ {ω | τ ω ≤ i}) :=
   Iff.rfl
 
 theorem measurableSpace_mono (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f π) (hle : τ ≤ π) :
@@ -475,7 +475,11 @@ theorem measurableSpace_mono (hτ : IsStoppingTime f τ) (hπ : IsStoppingTime f
     intro hle' _
     exact le_trans (hle _) hle'
 
-theorem measurableSpace_le (hτ : IsStoppingTime f τ) : hτ.measurableSpace ≤ m := fun _ hs ↦ hs.1
+theorem measurableSpace_le' (hτ : IsStoppingTime f τ) :
+    hτ.measurableSpace ≤ ⨆ t, f t := fun _ hs ↦ hs.1
+
+theorem measurableSpace_le (hτ : IsStoppingTime f τ) : hτ.measurableSpace ≤ m :=
+  hτ.measurableSpace_le'.trans (iSup_le f.le)
 
 @[simp]
 theorem measurableSpace_const (f : Filtration ι m) (i : ι) :
@@ -485,7 +489,7 @@ theorem measurableSpace_const (f : Filtration ι m) (i : ι) :
   constructor <;> intro h
   · have h' := h.2 i
     simpa only [le_refl, Set.ofPred_true, Set.inter_univ] using h'
-  · refine ⟨f.le i _ h, fun j ↦ ?_⟩
+  · refine ⟨le_iSup f i s h, fun j ↦ ?_⟩
     by_cases hij : i ≤ j
     · norm_cast
       simp only [hij, Set.ofPred_true, Set.inter_univ]
@@ -504,7 +508,7 @@ theorem measurableSet_inter_eq_iff (hτ : IsStoppingTime f τ) (s : Set Ω) (i :
     rw [hxi]
   constructor <;> intro h
   · simpa [Set.inter_assoc, this] using h.2 i
-  · refine ⟨f.le i _ h, fun j ↦ ?_⟩
+  · refine ⟨le_iSup f i _ h, fun j ↦ ?_⟩
     rw [Set.inter_assoc, this]
     by_cases hij : i ≤ j
     · norm_cast
@@ -550,7 +554,7 @@ variable [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → WithTop ι}
 
 protected theorem measurableSet_le' (hτ : IsStoppingTime f τ) (i : ι) :
     MeasurableSet[hτ.measurableSpace] {ω | τ ω ≤ i} := by
-  refine ⟨f.le i _ (hτ i), fun j ↦ ?_⟩
+  refine ⟨le_iSup f i _ (hτ i), fun j ↦ ?_⟩
   have : {ω : Ω | τ ω ≤ i} ∩ {ω : Ω | τ ω ≤ j} = {ω : Ω | τ ω ≤ min i j} := by
     ext1 ω
     simp [Set.mem_inter_iff, Set.mem_ofPred_eq]
@@ -649,11 +653,20 @@ protected theorem measurable' [TopologicalSpace ι]
     [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
     Measurable τ := hτ.measurable.mono (measurableSpace_le hτ) le_rfl
 
+protected theorem measurable_iSup [TopologicalSpace ι]
+    [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
+    Measurable[⨆ t, f t] τ := hτ.measurable.mono (measurableSpace_le' hτ) le_rfl
+
 protected lemma measurableSet_eq_top [TopologicalSpace ι]
     [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
     MeasurableSet {ω | τ ω = ⊤} :=
   (measurableSet_singleton _).preimage hτ.measurable'
 
+protected lemma measurableSet_eq_top' [TopologicalSpace ι]
+    [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) :
+    MeasurableSet[⨆ t, f t] {ω | τ ω = ⊤} :=
+  (measurableSet_singleton _).preimage hτ.measurable_iSup
+
 protected theorem measurable_of_le [TopologicalSpace ι]
     [OrderTopology ι] [SecondCountableTopology ι] (hτ : IsStoppingTime f τ) {i : ι}
     (hτ_le : ∀ ω, τ ω ≤ i) : Measurable[f i] τ :=
@@ -698,7 +711,7 @@ theorem measurableSet_inter_le [TopologicalSpace ι] [SecondCountableTopology ι
     ext ω
     by_cases hτi : τ ω ≤ i <;> grind
   simp_rw [h_eq]
-  refine ⟨hs.1.inter (measurableSet_le hτ.measurable' hπ.measurable'), fun i ↦ ?_⟩
+  refine ⟨hs.1.inter (measurableSet_le hτ.measurable_iSup hπ.measurable_iSup), fun i ↦ ?_⟩
   refine ((hs.2 i).inter ((hτ.min hπ) i)).inter ?_
   apply @measurableSet_le _ _ _ _ _ (Filtration.seq f i) _ _ _ _ _ ?_ ?_
   · exact (hτ.min_const i).measurable_of_le fun _ => min_le_right _ _
@@ -730,7 +743,7 @@ theorem measurableSet_le_stopping_time [TopologicalSpace ι] [SecondCountableTop
     [OrderTopology ι] (hτ : IsStoppingTime f τ)
     (hπ : IsStoppingTime f π) : MeasurableSet[hτ.measurableSpace] {ω | τ ω ≤ π ω} := by
   rw [hτ.measurableSet]
-  refine ⟨measurableSet_le hτ.measurable' hπ.measurable', fun j ↦ ?_⟩
+  refine ⟨measurableSet_le hτ.measurable_iSup hπ.measurable_iSup, fun j ↦ ?_⟩
   have : {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ j} = {ω | min (τ ω) j ≤ min (π ω) j} ∩ {ω | τ ω ≤ j} := by
     ext
     simpa using fun a b ↦ Std.IsPreorder.le_trans _ _ _ a b
@@ -1056,7 +1069,7 @@ theorem measurable_stoppedValue [PseudoMetrizableSpace β] [MeasurableSpace β]
       exact (h_seq_tendsto t).exists
   rw [this]
   refine MeasurableSet.union ?_ ?_
-  · exact MeasurableSet.iUnion fun i ↦ f.le (seq i) _
+  · exact MeasurableSet.iUnion fun i ↦ le_iSup f (seq i) _
       (measurableSet_preimage_stoppedValue_inter hf_prog hτ ht (seq i))
   · have : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω = ⊤}
        = (fun ω ↦ u (Classical.arbitrary ι) ω) ⁻¹' t ∩ {ω | τ ω = ⊤} := by
@@ -1066,9 +1079,9 @@ theorem measurable_stoppedValue [PseudoMetrizableSpace β] [MeasurableSpace β]
       intro h
       simp [h]
     rw [this]
-    refine MeasurableSet.inter (ht.preimage ?_) hτ.measurableSet_eq_top
+    refine MeasurableSet.inter (ht.preimage ?_) hτ.measurableSet_eq_top'
     exact (hf_prog.stronglyAdapted (Classical.arbitrary ι)).measurable.mono
-      (f.le (Classical.arbitrary ι)) le_rfl
+      (le_iSup f (Classical.arbitrary ι)) le_rfl
 
 end Progressive
 
diff --git a/Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean b/Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
index 9dbe2b156c..f1f82a6b59 100644
--- a/Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
+++ b/Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
@@ -5,7 +5,7 @@ Authors: Amelia Livingston, Yaël Dillies, Michał Mrugała
 -/
 module
 
-public import Mathlib.RingTheory.Bialgebra.Hom
+public import Mathlib.RingTheory.Bialgebra.Equiv
 public import Mathlib.RingTheory.Coalgebra.MonoidAlgebra
 
 /-!
@@ -87,6 +87,48 @@ lemma mapDomainBialgHom_mapDomainBialgHom (f : N →* O) (g : M →* N) (x : R[M
 
 end MonoidAlgebra
 
+namespace AddMonoidAlgebra
+variable [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M]
+
+variable (R A M) in
+/-- The bialgebra equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
+`Multiplicative`. -/
+-- TODO: Make `BialgEquiv.toCoalgEquiv` the simp normal form so that this can be simp
+@[simps! -isSimp]
+def toMultiplicativeBialgEquiv : A[M] ≃ₐc[R] MonoidAlgebra A (Multiplicative M) :=
+  .ofAlgEquiv (toMultiplicativeAlgEquiv R A M) (by ext <;> simp) <| by
+    ext a
+    · simp [Algebra.TensorProduct.one_def]
+    · simp [← (Coalgebra.Repr.arbitrary R a).eq]
+
+@[simp]
+lemma toMultiplicativeBialgEquiv_single (m : M) (a : A) :
+    toMultiplicativeBialgEquiv R A M (single m a) = .single (.ofAdd m) a := by
+  simp [toMultiplicativeBialgEquiv]
+
+end AddMonoidAlgebra
+
+namespace MonoidAlgebra
+variable [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M]
+
+variable (R A M) in
+/-- The bialgebra equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of
+`Additive`. -/
+-- TODO: Make `BialgEquiv.toCoalgEquiv` the simp normal form so that this can be simp
+@[simps! -isSimp]
+def toAdditiveBialgEquiv : A[M] ≃ₐc[R] AddMonoidAlgebra A (Additive M) :=
+  .ofAlgEquiv (toAdditiveAlgEquiv R A M) (by ext <;> simp) <| by
+    ext a
+    · simp [Algebra.TensorProduct.one_def]
+    · simp [← (Coalgebra.Repr.arbitrary R a).eq]
+
+@[simp]
+lemma toAdditiveBialgEquiv_single (m : M) (a : A) :
+    toAdditiveBialgEquiv R A M (single m a) = .single (.ofMul m) a := by
+  simp [toAdditiveBialgEquiv]
+
+end MonoidAlgebra
+
 namespace LaurentPolynomial
 
 open AddMonoidAlgebra
diff --git a/Mathlib/RingTheory/FiniteType.lean b/Mathlib/RingTheory/FiniteType.lean
index 0e3083e602..1ba1ee31b3 100644
--- a/Mathlib/RingTheory/FiniteType.lean
+++ b/Mathlib/RingTheory/FiniteType.lean
@@ -577,12 +577,12 @@ theorem freeAlgebra_lift_of_surjective_of_closure [CommSemiring R] {S : Set M}
 
 /-- If a monoid `M` is finitely generated then `R[M]` is of finite type. -/
 instance finiteType_of_fg [CommRing R] [Monoid.FG M] : FiniteType R R[M] :=
-  (AddMonoidAlgebra.finiteType_of_fg R (Additive M)).equiv (toAdditiveAlgEquiv R M).symm
+  (AddMonoidAlgebra.finiteType_of_fg R (Additive M)).equiv (toAdditiveAlgEquiv R R M).symm
 
 /-- A monoid `M` is finitely generated if and only if `R[M]` is of finite type. -/
 theorem finiteType_iff_fg [CommRing R] [Nontrivial R] : FiniteType R R[M] ↔ Monoid.FG M where
   mp h := Monoid.fg_iff_add_fg.2 <|
-    AddMonoidAlgebra.finiteType_iff_fg.1 <| h.equiv <| toAdditiveAlgEquiv R M
+    AddMonoidAlgebra.finiteType_iff_fg.1 <| h.equiv <| toAdditiveAlgEquiv R R M
   mpr _ := inferInstance
 
 /-- If `R[M]` is of finite type then `M` is finitely generated. -/
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
index 5f707e92f9..089c65ef76 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Group.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 module
 
 public import Mathlib.SetTheory.Cardinal.Finite
+public import Mathlib.Topology.Algebra.GroupWithZero
 public import Mathlib.Topology.Algebra.InfiniteSum.Basic
 public import Mathlib.Topology.UniformSpace.Cauchy
 public import Mathlib.Topology.Algebra.IsUniformGroup.Defs
@@ -415,8 +416,10 @@ theorem tprod_const [T2Space G] (a : G) : ∏' _ : β, a = a ^ (Nat.card β) :=
 end IsTopologicalGroup
 
 section CommGroupWithZero
-variable {K : Type*} [CommGroupWithZero K] [TopologicalSpace K] [SeparatelyContinuousMul K]
-  {f g : α → K}
+
+variable {K : Type*} [CommGroupWithZero K] [TopologicalSpace K]
+  {f g : α → K} {L : SummationFilter α}
+
 /-!
 ## Groups with a zero
 
@@ -424,6 +427,10 @@ These lemmas apply to a `CommGroupWithZero`; the most familiar case is when `K`
 are specific to the product setting and do not have a sensible additive analogue.
 -/
 
+section SeparatelyContinuousMul
+
+variable [SeparatelyContinuousMul K]
+
 open Finset in
 lemma HasProd.congr_cofinite₀ {c : K} (hc : HasProd f c) {s : Finset α}
     (hs : ∀ a ∈ s, f a ≠ 0) (hs' : ∀ a ∉ s, f a = g a) :
@@ -459,4 +466,36 @@ lemma Multipliable.congr_cofinite₀ (hf : Multipliable f) (hf' : ∀ a, f a ≠
   obtain ⟨s, hs⟩ : ∃ s : Finset α, ∀ i ∉ s, f i = g i := ⟨hfg.toFinset, by simp⟩
   exact (hc.congr_cofinite₀ (fun a _ ↦ hf' a) hs).multipliable
 
+end SeparatelyContinuousMul
+
+theorem HasProd.inv₀ {a : K} [ContinuousInv₀ K] (h : HasProd f a L) (ha : a ≠ 0) :
+    HasProd (fun x ↦ (f x)⁻¹) a⁻¹ L := by
+  simp_rw [HasProd, Finset.prod_inv_distrib]
+  exact Tendsto.inv₀ h ha
+
+theorem Multipliable.inv₀ [ContinuousInv₀ K] (h : Multipliable f L) (ne_zero : ∏'[L] x, f x ≠ 0) :
+    Multipliable (fun x ↦ (f x)⁻¹) L :=
+  h.hasProd.inv₀ ne_zero|>.multipliable
+
+theorem Multipliable.tprod_inv₀ [ContinuousInv₀ K] [T2Space K] [L.NeBot]
+    (h : Multipliable f L) (ne_zero : ∏'[L] x, f x ≠ 0) :
+    ∏'[L] x, (f x)⁻¹ = (∏'[L] x, f x )⁻¹ :=
+  h.hasProd.inv₀ ne_zero|>.tprod_eq
+
+theorem HasProd.div₀ [ContinuousInv₀ K] [ContinuousMul K] {a b : K}
+    (hf : HasProd f a L) (hg : HasProd g b L) (hb : b ≠ 0) :
+    HasProd (fun x ↦ f x / g x) (a / b) L := by
+  simp only [div_eq_mul_inv]
+  exact hf.mul <| hg.inv₀ hb
+
+theorem Multipliable.div₀ [ContinuousInv₀ K] [ContinuousMul K]
+    (hf : Multipliable f L) (hg : Multipliable g L) (ne_zero : ∏'[L] x, g x ≠ 0) :
+    Multipliable (fun x ↦ f x / g x) L :=
+  hf.hasProd.div₀ hg.hasProd ne_zero|>.multipliable
+
+theorem Multipliable.tprod_div₀ [ContinuousInv₀ K] [ContinuousMul K] [T2Space K] [L.NeBot]
+    (hf : Multipliable f L) (hg : Multipliable g L) (ne_zero : ∏'[L] x, g x ≠ 0) :
+    (∏'[L] x, f x / g x) = (∏'[L] x, f x) / (∏'[L] x, g x) :=
+  hf.hasProd.div₀ hg.hasProd ne_zero|>.tprod_eq
+
 end CommGroupWithZero
diff --git a/lake-manifest.json b/lake-manifest.json
index d4b1f3146e..ca62f89cbe 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "975a7ed3e5ed7838da79d5abddc50df73d0c84af",
+   "rev": "0a7a0cdc42f531e02361cb303b8cbf0e7d334f82",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/upstream_sha b/upstream_sha
index f4af490cd4..7342ae1e3e 100644
--- a/upstream_sha
+++ b/upstream_sha
@@ -1 +1 @@
-8e45b0548034eeda677a64e1e0b07837390835b6
+6c5a9081e9b704f0d366214e1fd5e68e1538a4b2