-- Mathlib/RingTheory/Nilpotent/Exp.lean
theorem exp_add_of_commute {a b : A} (h₁ : Commute a b) (h₂ : IsNilpotent a) (h₃ : IsNilpotent b) :
    exp (a + b) = exp a * exp b

Proof state:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
⊢ exp (a + b) = exp a * exp b

Tactic:
let N := n₁ ⊔ n₂

Result:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
⊢ exp (a + b) = exp a * exp b

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : (↑i !)⁻¹ * ↑(i.choose j) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹
⊢ (↑i !)⁻¹ • (a ^ j * b ^ (i - j) * ↑(i.choose j)) = ((↑j !)⁻¹ * (↑(i - j)!)⁻¹) • (a ^ j * b ^ (i - j))

Tactic:
rw [← Nat.cast_commute (i.choose j), ← this, ← Algebra.mul_smul_comm, ← nsmul_eq_mul,
  mul_smul, ← smul_assoc, smul_comm, smul_assoc]

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : (↑i !)⁻¹ * ↑(i.choose j) = (↑j !)⁻¹ * (↑(i - j)!)⁻¹
⊢ i.choose j • (↑i !)⁻¹ • (a ^ j * b ^ (i - j)) = ↑(i.choose j) • (↑i !)⁻¹ • (a ^ j * b ^ (i - j))

Proof state:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ :
  ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i =
    ∑ ij ∈ filter (fun ij => ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ filter (fun ij => ¬ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ filter (fun x => x.1 + x.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) +
      ∑ x ∈ filter (fun x => ¬x.1 + x.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
⊢ ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = (∑ i ∈ RN, (↑i !)⁻¹ • a ^ i) * ∑ i ∈ RN, (↑i !)⁻¹ • b ^ i

Tactic:
rw [z₁, add_zero] at split₁

Result:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ :
  ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i =
    ∑ ij ∈ filter (fun ij => ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ filter (fun ij => ¬ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ filter (fun x => x.1 + x.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
⊢ ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = (∑ i ∈ RN, (↑i !)⁻¹ • a ^ i) * ∑ i ∈ RN, (↑i !)⁻¹ • b ^ i

Proof state:
case refl
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
z₁ : ∑ ij ∈ filter (fun ij => ¬ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ filter (fun x => x.1 + x.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ :
  ∑ ij ∈ filter (fun ij => ¬(ij.1 ≤ N ∧ ij.2 ≤ N)) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ filter (fun x => x.1 ≤ N ∧ x.2 ≤ N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
restrict :
  ∑ ij ∈ filter (fun ij => ij.1 ≤ N ∧ ij.2 ≤ N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)
x✝¹ x✝ : (_ : ℕ) × ℕ
i j : ℕ
⊢ ⟨i, j⟩ = ⟨i, j⟩

Tactic:
rfl

Result:
no goals

Proof state:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₁ : ∑ ij ∈ filter (fun ij => ¬ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ filter (fun x => x.1 + x.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ :
  ∑ ij ∈ filter (fun ij => ¬(ij.1 ≤ N ∧ ij.2 ≤ N)) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
⊢ ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = (∑ i ∈ RN, (↑i !)⁻¹ • a ^ i) * ∑ i ∈ RN, (↑i !)⁻¹ • b ^ i

Tactic:
have split₂ := sum_filter_add_sum_filter_not (R2N ×ˢ R2N)
  (fun ij ↦ ij.1 ≤ N ∧ ij.2 ≤ N)
  (fun ij ↦ ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2))

Result:
case intro.intro
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
s₁ : ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₁ : ∑ ij ∈ filter (fun ij => ¬ij.1 + ij.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₁ :
  ∑ x ∈ filter (fun x => x.1 + x.2 ≤ 2 * N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
z₂ :
  ∑ ij ∈ filter (fun ij => ¬(ij.1 ≤ N ∧ ij.2 ≤ N)) (R2N ×ˢ R2N), ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0
split₂ :
  ∑ x ∈ filter (fun x => x.1 ≤ N ∧ x.2 ≤ N) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) +
      ∑ x ∈ filter (fun x => ¬(x.1 ≤ N ∧ x.2 ≤ N)) (R2N ×ˢ R2N), ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2) =
    ∑ x ∈ R2N ×ˢ R2N, ((↑x.1!)⁻¹ * (↑x.2!)⁻¹) • (a ^ x.1 * b ^ x.2)
⊢ ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = (∑ i ∈ RN, (↑i !)⁻¹ • a ^ i) * ∑ i ∈ RN, (↑i !)⁻¹ • b ^ i