[GOAL]
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.normalizer (toLieSubmodule H) = toLieSubmodule H
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff, coe_normalizer_eq_normalizer, IsCartanSubalgebra.self_normalizing,
  coe_toLieSubmodule]
[GOAL]
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
[PROOFSTEP]
induction' k with k ih
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
simp [ih]
[GOAL]
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)
[PROOFSTEP]
constructor
[GOAL]
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)
[PROOFSTEP]
intro h
[GOAL]
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)
[PROOFSTEP]
have h₁ : LieAlgebra.IsNilpotent R H := by infer_instance
[GOAL]
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 }
[PROOFSTEP]
infer_instance
[GOAL]
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)
[PROOFSTEP]
obtain ⟨k, hk⟩ := H.toLieSubmodule.isNilpotent_iff_exists_self_le_ucs.mp h₁
[GOAL]
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)
[PROOFSTEP]
replace hk : H.toLieSubmodule = LieSubmodule.ucs k ⊥ :=
  le_antisymm hk (LieSubmodule.ucs_le_of_normalizer_eq_self H.normalizer_eq_self_of_isCartanSubalgebra k)
[GOAL]
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)
[PROOFSTEP]
refine' ⟨k, fun l hl => _⟩
[GOAL]
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
[PROOFSTEP]
rw [← Nat.sub_add_cancel hl, LieSubmodule.ucs_add, ← hk, LieSubalgebra.ucs_eq_self_of_isCartanSubalgebra]
[GOAL]
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
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
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
[PROOFSTEP]
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] }
[GOAL]
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 }
[PROOFSTEP]
dsimp only [LieAlgebra.IsNilpotent]
[GOAL]
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 }
[PROOFSTEP]
erw [H.toLieSubmodule.isNilpotent_iff_exists_lcs_eq_bot]
[GOAL]
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) = ⊥
[PROOFSTEP]
use k
[GOAL]
case 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
⊢ LieSubmodule.lcs k (toLieSubmodule H) = ⊥
[PROOFSTEP]
rw [_root_.eq_bot_iff, LieSubmodule.lcs_le_iff, hk k (le_refl k)]
[GOAL]
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
[PROOFSTEP]
have hk' := hk (k + 1) k.le_succ
[GOAL]
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
[PROOFSTEP]
rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk' 
[GOAL]
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
[PROOFSTEP]
rw [← LieSubalgebra.coe_to_submodule_eq_iff, ← LieSubalgebra.coe_normalizer_eq_normalizer, hk',
  LieSubalgebra.coe_toLieSubmodule]
[GOAL]
R✝ : Type u
L✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : LieRing L✝
inst✝³ : LieAlgebra R✝ L✝
H : LieSubalgebra R✝ L✝
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ LieSubalgebra.normalizer (↑R L I) = ⊤
[PROOFSTEP]
ext x
[GOAL]
case h
R✝ : Type u
L✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : LieRing L✝
inst✝³ : LieAlgebra R✝ L✝
H : LieSubalgebra R✝ L✝
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ LieSubalgebra.normalizer (↑R L I) ↔ x ∈ ⊤
[PROOFSTEP]
simpa only [LieSubalgebra.mem_normalizer_iff, LieSubalgebra.mem_top, iff_true_iff] using fun y hy => I.lie_mem hy
[GOAL]
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : IsNilpotent R L
⊢ LieSubalgebra.normalizer ⊤ = ⊤
[PROOFSTEP]
rw [← top_coe_lieSubalgebra, normalizer_eq_top, top_coe_lieSubalgebra]
