-- 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 calc_2
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 ∈ RN.sigma fun i => RN, ((↑x.fst !)⁻¹ * (↑x.snd !)⁻¹) • (a ^ x.fst * b ^ x.snd) =
    ∑ ij ∈ RN ×ˢ RN, ((↑ij.1!)⁻¹ * (↑ij.2!)⁻¹) • (a ^ ij.1 * b ^ ij.2)

Tactic:
apply sum_bijective (fun ⟨i, j⟩ ↦ (i, j))

Result:
case calc_2.he
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)
⊢ Function.Bijective fun x =>
    match x with
    | ⟨i, j⟩ => (i, j)

case calc_2.hst
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)
⊢ ∀ (i : (_ : ℕ) × ℕ),
    (i ∈ RN.sigma fun i => RN) ↔
      (match i with
        | ⟨i, j⟩ => (i, j)) ∈
        RN ×ˢ RN

case calc_2.hfg
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)
⊢ ∀ i ∈ RN.sigma fun i => RN,
    ((↑i.fst !)⁻¹ * (↑i.snd !)⁻¹) • (a ^ i.fst * b ^ i.snd) =
      ((↑(match i with
                  | ⟨i, j⟩ => (i, j)).1!)⁻¹ *
          (↑(match i with
                  | ⟨i, j⟩ => (i, j)).2!)⁻¹) •
        (a ^
            (match i with
              | ⟨i, j⟩ => (i, j)).1 *
          b ^
            (match i with
              | ⟨i, j⟩ => (i, j)).2)