-- Module: Mathlib.RingTheory.Nilpotent.Exp
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))
calc_2 :
  Function.Bijective (β := ℕ × ℕ) fun (x : (_ : ℕ) × ℕ) ↦
    match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) x with
    | ⟨i, j⟩ => (i, j)
calc_2₁ :
  ∀ (i : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) (RN.sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ RN) i ↔
      Membership.mem (α := ℕ × ℕ) (RN ×ˢ RN)
        (match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) i with
          | ⟨i, j⟩ => (i, j) :
          ℕ × ℕ)
calc_2₂ :
  ∀ (i : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) (RN.sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ RN) i →
      HMul.hMul (α := ℚ) (↑i.fst (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹ (↑i.snd (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹ •
          (a ^ i.fst (β := fun (i : ℕ) ↦ ℕ) * b ^ i.snd (β := fun (i : ℕ) ↦ ℕ)) =
        HMul.hMul (α := ℚ)
            (↑(match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) i with
                      | ⟨i, j⟩ => (i, j)).1! :
                ℚ)⁻¹
            (↑(match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) i with
                      | ⟨i, j⟩ => (i, j)).2! :
                ℚ)⁻¹ •
          (HPow.hPow (β := ℕ) a
              (match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) i with
                | ⟨i, j⟩ => (i, j)).1 *
            HPow.hPow (β := ℕ) b
              (match (motive := (_ : ℕ) × ℕ → ℕ × ℕ) i with
                | ⟨i, j⟩ => (i, j)).2)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ x ∈ RN.sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ RN,
      HMul.hMul (α := ℚ) (↑x.fst (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹ (↑x.snd (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹ •
        (a ^ x.fst (β := fun (i : ℕ) ↦ ℕ) * b ^ x.snd (β := fun (i : ℕ) ↦ ℕ)))
    (∑ ij ∈ RN ×ˢ RN, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))

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

Premises used: Finset.sum_bijective