-- Mathlib/Algebra/Lie/Weights/Cartan.lean
lemma toEnd_pow_apply_mem {χ₁ χ₂ : H → R} {x : L} {m : M}
    (hx : x ∈ rootSpace H χ₁) (hm : m ∈ genWeightSpace M χ₂) (n) :
    (toEnd R L M x ^ n : Module.End R M) m ∈ genWeightSpace M (n • χ₁ + χ₂)

Proof state:
case h.e'_4.h.e'_12
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
n : ℕ
IH : ((toEnd R L M) x ^ n) m ∈ genWeightSpace M (n • χ₁ + χ₂)
⊢ (n + 1) • χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)

Tactic:
rw [succ_nsmul, ← add_assoc, add_comm (n • _)]

Result:
no goals

Proof state:
case succ
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
n : ℕ
IH : ((toEnd R L M) x ^ n) m ∈ genWeightSpace M (n • χ₁ + χ₂)
⊢ ((toEnd R L M) x ^ (n + 1)) m ∈ genWeightSpace M ((n + 1) • χ₁ + χ₂)

Tactic:
simp only [pow_succ', LinearMap.mul_apply, toEnd_apply_apply,
  Nat.cast_add, Nat.cast_one, rootSpace]

Result:
case succ
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
n : ℕ
IH : ((toEnd R L M) x ^ n) m ∈ genWeightSpace M (n • χ₁ + χ₂)
⊢ ⁅x, ((toEnd R L M) x ^ n) m⁆ ∈ genWeightSpace M ((n + 1) • χ₁ + χ₂)

Proof state:
case zero
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
⊢ ((toEnd R L M) x ^ 0) m ∈ genWeightSpace M (0 • χ₁ + χ₂)

Tactic:
simpa using hm

Result:
no goals

Proof state:
case succ
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
n : ℕ
IH : ((toEnd R L M) x ^ n) m ∈ genWeightSpace M (n • χ₁ + χ₂)
⊢ ⁅x, ((toEnd R L M) x ^ n) m⁆ ∈ genWeightSpace M ((n + 1) • χ₁ + χ₂)

Tactic:
convert lie_mem_genWeightSpace_of_mem_genWeightSpace hx IH using 2

Result:
case h.e'_4.h.e'_12
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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
n : ℕ
IH : ((toEnd R L M) x ^ n) m ∈ genWeightSpace M (n • χ₁ + χ₂)
⊢ (n + 1) • χ₁ + χ₂ = χ₁ + (n • χ₁ + χ₂)

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
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : ↥H → R
x : L
m : M
hx : x ∈ rootSpace H χ₁
hm : m ∈ genWeightSpace M χ₂
n : ℕ
⊢ ((toEnd R L M) x ^ n) m ∈ genWeightSpace M (n • χ₁ + χ₂)

Tactic:
induction n with
| zero => simpa using hm
| succ n IH =>
  simp only [pow_succ', LinearMap.mul_apply, toEnd_apply_apply,
    Nat.cast_add, Nat.cast_one, rootSpace]
  convert lie_mem_genWeightSpace_of_mem_genWeightSpace hx IH using 2
  rw [succ_nsmul, ← add_assoc, add_comm (n • _)]

Result:
no goals