-- Mathlib/Algebra/Lie/Sl2.lean
lemma pow_toEnd_f_ne_zero_of_eq_nat
    [CharZero R] [NoZeroSMulDivisors R M]
    {n : ℕ} (hn : μ = n) {i} (hi : i ≤ n) : (ψ i) ≠ 0

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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : n = i ∨ ((toEnd R L M) f ^ i) m = 0
⊢ False

Tactic:
exact (hi.trans_eq (this.resolve_right (IH (i.le_succ.trans hi)))).not_lt i.lt_succ_self

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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
hi : 0 ≤ n
H : ((toEnd R L M) f ^ 0) m = 0
⊢ m = 0

Tactic:
simpa using 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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : ((↑i + 1) * (↑n - ↑i)) • ((toEnd R L M) f ^ i) m = 0
⊢ False

Tactic:
rw [← Int.cast_smul_eq_zsmul R, smul_eq_zero, Int.cast_eq_zero, mul_eq_zero, sub_eq_zero,
  Nat.cast_inj, ← @Nat.cast_one ℤ, ← Nat.cast_add, Nat.cast_eq_zero] at this

Result:
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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : (i + 1 = 0 ∨ n = i) ∨ ((toEnd R L M) f ^ i) m = 0
⊢ False

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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : (fun x => ⁅e, x⁆) (((toEnd R L M) f ^ (i + 1)) m) = (fun x => ⁅e, x⁆) 0
⊢ ((↑i + 1) * (↑n - ↑i)) • ((toEnd R L M) f ^ i) m = 0

Tactic:
simpa [← Int.cast_smul_eq_zsmul R, P.lie_e_pow_succ_toEnd_f, hn] using this

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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
i : ℕ
hi : i ≤ n
H : ((toEnd R L M) f ^ i) m = 0
⊢ False

Tactic:
induction i

Result:
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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
hi : 0 ≤ n
H : ((toEnd R L M) f ^ 0) m = 0
⊢ False

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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
n✝ : ℕ
a✝ : n✝ ≤ n → ((toEnd R L M) f ^ n✝) m = 0 → False
hi : n✝ + 1 ≤ n
H : ((toEnd R L M) f ^ (n✝ + 1)) m = 0
⊢ False

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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
hi : 0 ≤ n
H : ((toEnd R L M) f ^ 0) m = 0
⊢ False

Tactic:
exact P.ne_zero (by simpa using 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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
i : ℕ
hi : i ≤ n
⊢ ((toEnd R L M) f ^ i) m ≠ 0

Tactic:
intro H

Result:
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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
i : ℕ
hi : i ≤ n
H : ((toEnd R L M) f ^ i) m = 0
⊢ False

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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : (i + 1 = 0 ∨ n = i) ∨ ((toEnd R L M) f ^ i) m = 0
⊢ False

Tactic:
simp only [add_eq_zero, one_ne_zero, and_false, false_or] at this

Result:
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 μ
inst✝¹ : CharZero R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : μ = ↑n
i : ℕ
IH : i ≤ n → ((toEnd R L M) f ^ i) m = 0 → False
hi : i + 1 ≤ n
H : ((toEnd R L M) f ^ (i + 1)) m = 0
this : n = i ∨ ((toEnd R L M) f ^ i) m = 0
⊢ False