case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ IsCartanSubalgebra H → LieSubmodule.IsUcsLimit (toLieSubmodule H)

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H) → IsCartanSubalgebra H
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ IsCartanSubalgebra H ↔ LieSubmodule.IsUcsLimit (toLieSubmodule H)
constructor
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ IsCartanSubalgebra H → LieSubmodule.IsUcsLimit (toLieSubmodule H)
intro h
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
have h₁ : LieAlgebra.IsNilpotent R H := by infer_instance
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
k : ℕ
hk : toLieSubmodule H ≤ LieSubmodule.ucs k ⊥
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
obtain ⟨k, hk⟩ := H.toLieSubmodule.isNilpotent_iff_exists_self_le_ucs.mp h₁
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
k : ℕ
hk : toLieSubmodule H = LieSubmodule.ucs k ⊥
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
k : ℕ
hk : toLieSubmodule H ≤ LieSubmodule.ucs k ⊥
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
replace hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥ :=
  le_antisymm hk
    (LieSubmodule.ucs_le_of_normalizer_eq_self H.normalizer_eq_self_of_isCartanSubalgebra k)
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
k : ℕ
hk : toLieSubmodule H = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ LieSubmodule.ucs l ⊥ = toLieSubmodule H
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
k : ℕ
hk : toLieSubmodule H = LieSubmodule.ucs k ⊥
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H)
refine' ⟨k, fun l hl => _⟩
no goals
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
h₁ : LieAlgebra.IsNilpotent R { x // x ∈ H }
k : ℕ
hk : toLieSubmodule H = LieSubmodule.ucs k ⊥
l : ℕ
hl : k ≤ l
⊢ LieSubmodule.ucs l ⊥ = toLieSubmodule H
rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk,
  LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]
no goals
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : IsCartanSubalgebra H
⊢ LieAlgebra.IsNilpotent R { x // x ∈ H }
infer_instance
case mpr.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ IsCartanSubalgebra H
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ LieSubmodule.IsUcsLimit (toLieSubmodule H) → IsCartanSubalgebra H
rintro ⟨k, hk⟩
no goals
case mpr.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ IsCartanSubalgebra H
exact
  { nilpotent := by
      dsimp only [LieAlgebra.IsNilpotent]
      erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]
      use k
      rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
    self_normalizing := by
      have hk' := hk (k + 1) k.le_succ
      rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'
      rw [← LieSubalgebra.coe_to_submodule_eq_iff, ← LieSubalgebra.coe_normalizer_eq_normalizer,
        hk', LieSubalgebra.coe_toLieSubmodule] }
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ LieModule.IsNilpotent R { x // x ∈ H } { x // x ∈ H }
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ LieAlgebra.IsNilpotent R { x // x ∈ H }
dsimp only [LieAlgebra.IsNilpotent]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ ∃ k, LieSubmodule.lcs k (toLieSubmodule H) = ⊥
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ LieModule.IsNilpotent R { x // x ∈ H } { x // x ∈ H }
erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ LieSubmodule.lcs k (toLieSubmodule H) = ⊥
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ ∃ k, LieSubmodule.lcs k (toLieSubmodule H) = ⊥
use k
no goals
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ LieSubmodule.lcs k (toLieSubmodule H) = ⊥
rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
hk' : LieSubmodule.ucs (k + 1) ⊥ = toLieSubmodule H
⊢ normalizer H = H
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
⊢ normalizer H = H
have hk' := hk (k + 1) k.le_succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
hk' : LieSubmodule.normalizer (toLieSubmodule H) = toLieSubmodule H
⊢ normalizer H = H
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
hk' : LieSubmodule.ucs (k + 1) ⊥ = toLieSubmodule H
⊢ normalizer H = H
rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'
no goals
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = toLieSubmodule H
hk' : LieSubmodule.normalizer (toLieSubmodule H) = toLieSubmodule H
⊢ normalizer H = H
rw [← LieSubalgebra.coe_to_submodule_eq_iff, ← LieSubalgebra.coe_normalizer_eq_normalizer,
  hk', LieSubalgebra.coe_toLieSubmodule]