-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max 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₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
z₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₁ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
z₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N),
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    0
split₂ :
  Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
restrict :
  Eq.{u_1 + 1} (α := A)
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
s₂ :
  HMul.hMul (α := A) (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i)) =
    ∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2)
⊢ ∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HMul.hMul (α := A) (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
have rwa : ∀
  (s₁ :
    ∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
      HMul.hMul (α := A) (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
        (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i)))
  (z₁ :
    Eq.{u_1 + 1} (α := A)
      (∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N,
        HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
      0)
  (split₁ :
    Eq.{u_1 + 1} (α := A)
      (∑ x ∈ R2N ×ˢ R2N with x.1 + x.2 ≤ 2 * N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
      (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2)))
  (z₂ :
    Eq.{u_1 + 1} (α := A)
      (∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N),
        HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
      0)
  (split₂ :
    Eq.{u_1 + 1} (α := A)
      (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
      (∑ x ∈ R2N ×ˢ R2N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2)))
  (restrict :
    Eq.{u_1 + 1} (α := A)
      (∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N,
        HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
      (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2)))
  (s₂ :
    HMul.hMul (α := A) (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
        (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i)) =
      ∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2)),
  ∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HMul.hMul (α := A) (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ RN, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
Tactic: rwa [s₂.symm] at s₁
Cleared hypotheses: s₁, z₁, split₁, z₂, split₂, restrict, s₂