-- 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)
calc_3 :
  ∀ (a : (_ : ℕ) × ℕ)
    (ha :
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) a),
    Membership.mem (α := ℕ × ℕ) ({ij ∈ range (2 * N + 1) ×ˢ range (2 * N + 1) | ij.1 + ij.2 ≤ 2 * N})
      (match (motive :=
          (x : (_ : ℕ) × ℕ) →
            Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
                ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) x →
              ℕ × ℕ)
          a, ha with
        | ⟨i, j⟩, x => (j, i - j) :
        ℕ × ℕ)
calc_3₁ :
  ∀ (a₁ : (_ : ℕ) × ℕ)
    (ha₁ :
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) a₁)
    (a₂ : (_ : ℕ) × ℕ)
    (ha₂ :
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) a₂),
    Eq (α := ℕ × ℕ)
        (match (motive :=
            (x : (_ : ℕ) × ℕ) →
              Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
                  ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) x →
                ℕ × ℕ)
            a₁, ha₁ with
          | ⟨i, j⟩, x => (j, i - j) :
          ℕ × ℕ)
        (match (motive :=
            (x : (_ : ℕ) × ℕ) →
              Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
                  ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) x →
                ℕ × ℕ)
            a₂, ha₂ with
          | ⟨i, j⟩, x => (j, i - j) :
          ℕ × ℕ) →
      a₁ = a₂
calc_3₂ :
  ∀ b ∈ {ij ∈ range (2 * N + 1) ×ˢ range (2 * N + 1) | ij.1 + ij.2 ≤ 2 * N},
    ∃ (a : (_ : ℕ) × ℕ) (ha :
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) a),
      (match (motive :=
          (x : (_ : ℕ) × ℕ) →
            Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
                ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) x →
              ℕ × ℕ)
          a, ha with
        | ⟨i, j⟩, x => (j, i - j)) =
        b
⊢ Eq.{u_1 + 1} (α := A)
    (∑ x ∈ (range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1),
      HMul.hMul (α := ℚ) (↑x.snd (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹
          (↑(x.fst (β := fun (i : ℕ) ↦ ℕ) - x.snd (β := fun (i : ℕ) ↦ ℕ))! : ℚ)⁻¹ •
        (a ^ x.snd (β := fun (i : ℕ) ↦ ℕ) * b ^ (x.fst (β := fun (i : ℕ) ↦ ℕ) - x.snd (β := fun (i : ℕ) ↦ ℕ))))
    (∑ ij ∈ range (2 * N + 1) ×ˢ range (2 * N + 1) with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
have calc_3₃ : ∀ (a_1 : (_ : ℕ) × ℕ)
  (ha :
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
      ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) a_1),
  HMul.hMul (α := ℚ) (↑a_1.snd (β := fun (i : ℕ) ↦ ℕ)! : ℚ)⁻¹
        (↑(a_1.fst (β := fun (i : ℕ) ↦ ℕ) - a_1.snd (β := fun (i : ℕ) ↦ ℕ))! : ℚ)⁻¹ •
      (a ^ a_1.snd (β := fun (i : ℕ) ↦ ℕ) * b ^ (a_1.fst (β := fun (i : ℕ) ↦ ℕ) - a_1.snd (β := fun (i : ℕ) ↦ ℕ))) =
    HMul.hMul (α := ℚ)
        (↑(match (motive :=
                    (x : (_ : ℕ) × ℕ) →
                      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
                          ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) x →
                        ℕ × ℕ)
                    a_1, ha with
                  | ⟨i, j⟩, x => (j, i - j)).1! :
            ℚ)⁻¹
        (↑(match (motive :=
                    (x : (_ : ℕ) × ℕ) →
                      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
                          ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) x →
                        ℕ × ℕ)
                    a_1, ha with
                  | ⟨i, j⟩, x => (j, i - j)).2! :
            ℚ)⁻¹ •
      (HPow.hPow (β := ℕ) a
          (match (motive :=
              (x : (_ : ℕ) × ℕ) →
                Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
                    ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) x →
                  ℕ × ℕ)
              a_1, ha with
            | ⟨i, j⟩, x => (j, i - j)).1 *
        HPow.hPow (β := ℕ) b
          (match (motive :=
              (x : (_ : ℕ) × ℕ) →
                Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
                    ((range (2 * N + 1)).sigma (α := fun (a : ℕ) ↦ ℕ) fun (i : ℕ) ↦ range (i + 1)) x →
                  ℕ × ℕ)
              a_1, ha with
            | ⟨i, j⟩, x => (j, i - j)).2)
Tactic: apply sum_bij (fun ⟨i, j⟩ _ ↦ (j, i - j))