-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem zeroRootSubalgebra_normalizer_eq_self :
    (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ (zeroRootSubalgebra R L H).normalizer
⊢ x ∈ zeroRootSubalgebra R L H

Tactic:
rw [LieSubalgebra.mem_normalizer_iff] at hx

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
⊢ x ∈ zeroRootSubalgebra R L H

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
⊢ (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H

Tactic:
refine le_antisymm ?_ (LieSubalgebra.le_normalizer _)

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
⊢ (zeroRootSubalgebra R L H).normalizer ≤ zeroRootSubalgebra R L H

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
⊢ ∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) x = 0

Tactic:
rintro ⟨y, hy⟩

Result:
case mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
y : L
hy : y ∈ H
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
⊢ (zeroRootSubalgebra R L H).normalizer ≤ zeroRootSubalgebra R L H

Tactic:
intro x hx

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ (zeroRootSubalgebra R L H).normalizer
⊢ x ∈ zeroRootSubalgebra R L H

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
⊢ x ∈ zeroRootSubalgebra R L H

Tactic:
rw [mem_zeroRootSubalgebra]

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
⊢ ∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) x = 0

Proof state:
case mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Tactic:
obtain ⟨k, hk⟩ := hx ⟨y, hy⟩

Result:
case mk.intro
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅x, y⁆ = 0
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Proof state:
case mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
y : L
hy : y ∈ H
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Tactic:
specialize hx y (le_zeroRootSubalgebra R L H hy)

Result:
case mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Proof state:
case mk.intro
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅x, y⁆ = 0
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Tactic:
rw [← lie_skew, LinearMap.map_neg, neg_eq_zero] at hk

Result:
case mk.intro
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Proof state:
case mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ⁅x, y⁆ ∈ zeroRootSubalgebra R L H
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Tactic:
rw [mem_zeroRootSubalgebra] at hx

Result:
case mk
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Proof state:
case mk.intro
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) x = 0

Tactic:
use k + 1

Result:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ((toEnd R (↥H) L) ⟨y, hy⟩ ^ (k + 1)) x = 0

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x y : L
hy : y ∈ H
hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0
k : ℕ
hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0
⊢ ((toEnd R (↥H) L) ⟨y, hy⟩ ^ (k + 1)) x = 0

Tactic:
rw [LinearMap.iterate_succ, LinearMap.coe_comp, Function.comp_apply, toEnd_apply_apply,
  LieSubalgebra.coe_bracket_of_module, Submodule.coe_mk, hk]

Result:
no goals