-- Mathlib/RingTheory/Nilpotent/Exp.lean
theorem exp_eq_truncated {a : A} {k : ℕ}  (h : a ^ k = 0) :
    ∑ i ∈ range k, (i.factorial : ℚ)⁻¹ • (a ^ i) = exp a

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
⊢ ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i = exp a

Tactic:
suffices ∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) = 0 by
  dsimp [exp]
  rw [h₁, this, add_zero]

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
⊢ ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
this : ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
⊢ ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i = ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i

Tactic:
rw [h₁, this, add_zero]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
x✝ : ℕ
h₂ : x✝ ∈ Ico (nilpotencyClass a) k
⊢ (↑x✝!)⁻¹ • a ^ x✝ = 0

Tactic:
rw [pow_eq_zero_of_le (mem_Ico.1 h₂).1 (pow_nilpotencyClass ⟨k, h⟩), smul_zero]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
k : ℕ
h : a ^ k = 0
⊢ ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i = exp a

Tactic:
have h₁ : ∑ i ∈ range k, (i.factorial : ℚ)⁻¹ • (a ^ i) =
    ∑ i ∈ range (nilpotencyClass a), (i.factorial : ℚ)⁻¹ • (a ^ i) +
      ∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) :=
  (sum_range_add_sum_Ico _ (csInf_le' h)).symm

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
⊢ ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i = exp a

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
⊢ ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0

Tactic:
exact sum_eq_zero fun _ h₂ => by
  rw [pow_eq_zero_of_le (mem_Ico.1 h₂).1 (pow_nilpotencyClass ⟨k, h⟩), smul_zero]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
this : ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
⊢ ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i = exp a

Tactic:
dsimp [exp]

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
this : ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
⊢ ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i = ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i