case zero
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
⊢ LieSubmodule.ucs Nat.zero (toLieSubmodule H) = toLieSubmodule H

case succ
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
k : ℕ
ih : LieSubmodule.ucs k (toLieSubmodule H) = toLieSubmodule H
⊢ LieSubmodule.ucs (Nat.succ k) (toLieSubmodule H) = toLieSubmodule H
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
k : ℕ
⊢ LieSubmodule.ucs k (toLieSubmodule H) = toLieSubmodule H
induction' k with k ih
no goals
case zero
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
⊢ LieSubmodule.ucs Nat.zero (toLieSubmodule H) = toLieSubmodule H
simp
no goals
case succ
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H✝ H : LieSubalgebra R L
inst✝ : IsCartanSubalgebra H
k : ℕ
ih : LieSubmodule.ucs k (toLieSubmodule H) = toLieSubmodule H
⊢ LieSubmodule.ucs (Nat.succ k) (toLieSubmodule H) = toLieSubmodule H
simp [ih]