-- Mathlib/Algebra/Lie/Sl2.lean
lemma lie_h_pow_toEnd_f (n : ℕ) :
    ⁅h, ψ n⁆ = (μ - 2 * n) • ψ n

Proof state:
case succ
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ (-2 + (μ - 2 * ↑n)) • ⁅f, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * (↑n + 1)) • ⁅f, ((toEnd R L M) f ^ n) m⁆

Tactic:
congr

Result:
case succ.e_a
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ -2 + (μ - 2 * ↑n) = μ - 2 * (↑n + 1)

Proof state:
case succ
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ ⁅h, ((toEnd R L M) f ^ (n + 1)) m⁆ = (μ - 2 * ↑(n + 1)) • ((toEnd R L M) f ^ (n + 1)) m

Tactic:
rw [pow_succ', LinearMap.mul_apply, toEnd_apply_apply, Nat.cast_add, Nat.cast_one,
  leibniz_lie h, t.lie_lie_smul_f R, ← neg_smul, ih, lie_smul, smul_lie, ← add_smul]

Result:
case succ
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ (-2 + (μ - 2 * ↑n)) • ⁅f, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * (↑n + 1)) • ⁅f, ((toEnd R L M) f ^ n) m⁆

Proof state:
case zero
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
⊢ ⁅h, ((toEnd R L M) f ^ 0) m⁆ = (μ - 2 * ↑0) • ((toEnd R L M) f ^ 0) m

Tactic:
simpa using P.lie_h

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
⊢ ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m

Tactic:
induction n with
| zero => simpa using P.lie_h
| succ n ih =>
  rw [pow_succ', LinearMap.mul_apply, toEnd_apply_apply, Nat.cast_add, Nat.cast_one,
    leibniz_lie h, t.lie_lie_smul_f R, ← neg_smul, ih, lie_smul, smul_lie, ← add_smul]
  congr
  ring

Result:
no goals

Proof state:
case succ.e_a
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
ih : ⁅h, ((toEnd R L M) f ^ n) m⁆ = (μ - 2 * ↑n) • ((toEnd R L M) f ^ n) m
⊢ -2 + (μ - 2 * ↑n) = μ - 2 * (↑n + 1)

Tactic:
ring

Result:
no goals