awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ exp (a + b) = exp a * exp b
have rw : ∑ i ∈ range (2 * N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
  HMul.hMul (α := A) (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
    (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
Tactic: rw [exp_eq_sum (k := 2 * N + 1)
    (Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero h₁ h₄ h₅ (by lia)),
    exp_eq_sum h₄, exp_eq_sum h₅]
-- 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
⊢ ∑ i ∈ range (2 * N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HMul.hMul (α := A) (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
have set : let R2N := range (2 * N + 1);
∀ (hR2N : R2N = range (2 * N + 1)),
  ∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HMul.hMul (α := A) (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
Tactic: set R2N := range (2 * N + 1) with hR2N
-- 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)
⊢ ∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HMul.hMul (α := A) (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ i))
      (∑ i ∈ range (N + 1), HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (b ^ i))
have set : let RN := range (N + 1);
∀ (hRN : RN = range (N + 1)),
  ∑ 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: set RN := range (N + 1) with hRN
-- 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)
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
have calc_1 : Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
  (∑ i ∈ R2N,
    HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A)))
Tactic: calc ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • (a + b) ^ i
        = ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * i.choose j := ?_
      _ = ∑ i ∈ R2N, (∑ j ∈ range (i + 1),
            ((j ! : ℚ)⁻¹ * ((i - j) ! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_
      _ = ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
            ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
-- 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_1 :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ i ∈ R2N,
      HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A)))
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
have calc_2 : Eq.{u_1 + 1} (α := A)
  (∑ i ∈ R2N,
    HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A)))
  (∑ i ∈ R2N, ∑ j ∈ range (i + 1), HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j)))
Tactic: calc ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • (a + b) ^ i
        = ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * i.choose j := ?_
      _ = ∑ i ∈ R2N, (∑ j ∈ range (i + 1),
            ((j ! : ℚ)⁻¹ * ((i - j) ! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_
      _ = ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
            ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
-- 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_1 :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ i ∈ R2N,
      HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A)))
calc_2 :
  Eq.{u_1 + 1} (α := A)
    (∑ i ∈ R2N,
      HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A)))
    (∑ i ∈ R2N, ∑ j ∈ range (i + 1), HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j)))
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
have calc_3 : Eq.{u_1 + 1} (α := A)
  (∑ i ∈ R2N, ∑ j ∈ range (i + 1), HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j)))
  (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
Tactic: calc ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • (a + b) ^ i
        = ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * i.choose j := ?_
      _ = ∑ i ∈ R2N, (∑ j ∈ range (i + 1),
            ((j ! : ℚ)⁻¹ * ((i - j) ! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_
      _ = ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
            ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
-- 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)
⊢ Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ i ∈ R2N,
      HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A)))
have calc_1 : ∀ i ∈ R2N,
  HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A))
Tactic: refine sum_congr rfl fun i _ ↦ ?_
-- 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)
i : ℕ
h : i ∈ R2N
⊢ HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A))
have calc_1 : HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ m ∈ range (i + 1), a ^ m * b ^ (i - m) * (↑(i.choose m) : A)) =
  HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A))
Tactic: rw [Commute.add_pow h₁ i]
-- 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)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ i ∈ R2N,
      HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A)))
    (∑ i ∈ R2N, ∑ j ∈ range (i + 1), HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j)))
have calc_2 : Eq.{u_1 + 1} (α := A)
  (∑ x ∈ R2N,
    ∑ x_1 ∈ range (x + 1), HSMul.hSMul (α := ℚ) (↑x ! : ℚ)⁻¹ (a ^ x_1 * b ^ (x - x_1) * (↑(x.choose x_1) : A)))
  (∑ i ∈ R2N, ∑ j ∈ range (i + 1), HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j)))
Tactic: simp_rw [smul_sum]
-- 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)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ x ∈ R2N,
      ∑ x_1 ∈ range (x + 1), HSMul.hSMul (α := ℚ) (↑x ! : ℚ)⁻¹ (a ^ x_1 * b ^ (x - x_1) * (↑(x.choose x_1) : A)))
    (∑ i ∈ R2N, ∑ j ∈ range (i + 1), HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j)))
have calc_2 : ∀ (i : ℕ) (hi : i ∈ R2N) (j : ℕ) (hj : j ∈ range (i + 1)),
  HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j) * (↑(i.choose j) : A)) =
    HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j))
Tactic: refine sum_congr rfl fun i hi ↦ sum_congr rfl fun j hj ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ∈ range (i + 1)
⊢ HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j) * (↑(i.choose j) : A)) =
    HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j))
have hj₁ : j < i + 1
Tactic: simp only [mem_range] at hi hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.RingTheory.Nilpotent.Exp (hypothesis)
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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j < i + 1
⊢ HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j) * (↑(i.choose j) : A)) =
    HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j))
have hj₁ : j ≤ i
Tactic: replace hj := Nat.le_of_lt_succ hj
Cleared hypotheses: hj
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : HMul.hMul (α := ℚ) (↑i ! : ℚ)⁻¹ (↑(i.choose j) : ℚ) = HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹
⊢ HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j) * (↑(i.choose j) : A)) =
    HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j))
have rw : i.choose j • HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j)) =
  HSMul.hSMul (α := ℚ) (↑(i.choose j) : ℚ) (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j)))
Tactic: rw [← Nat.cast_commute (i.choose j), ← this, ← mul_smul_comm, ← nsmul_eq_mul,
          mul_smul, ← smul_assoc, smul_comm, smul_assoc]
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : HMul.hMul (α := ℚ) (↑i ! : ℚ)⁻¹ (↑(i.choose j) : ℚ) = HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹
⊢ i.choose j • HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j)) =
    HSMul.hSMul (α := ℚ) (↑(i.choose j) : ℚ) (HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j)))
have norm_cast : i.choose j • HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j)) =
  i.choose j • HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j))
Tactic: norm_cast
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j) * (↑(i.choose j) : A)) =
    HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j))
have calc_2 : HMul.hMul (α := ℚ) (↑i ! : ℚ)⁻¹ (↑(i.choose j) : ℚ) = HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹
Tactic: suffices (i ! : ℚ)⁻¹ * (i.choose j) = ((j ! : ℚ)⁻¹ * ((i - j)! : ℚ)⁻¹) by
        rw [← Nat.cast_commute (i.choose j), ← this, ← mul_smul_comm, ← nsmul_eq_mul,
          mul_smul, ← smul_assoc, smul_comm, smul_assoc]
        norm_cast
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ HMul.hMul (α := ℚ) (↑i ! : ℚ)⁻¹ (↑(i.choose j) : ℚ) = HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹
have calc_2 : (↑i ! : ℚ)⁻¹ * HDiv.hDiv (α := ℚ) (↑i ! : ℚ) (↑(j ! * (i - j)!) : ℚ) = HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹
Tactic: rw [Nat.choose_eq_factorial_div_factorial hj,
        Nat.cast_div (Nat.factorial_mul_factorial_dvd_factorial hj) (by positivity)]
-- 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)
⊢ Eq.{u_1 + 1} (α := A)
    (∑ i ∈ R2N, ∑ j ∈ range (i + 1), HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (a ^ j * b ^ (i - j)))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
have calc_3 : 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))
Tactic: rw [hR2N, sum_sigma']
-- 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)
⊢ 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 : (_ : ℕ) × ℕ)
  (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) :
      ℕ × ℕ)
Tactic: apply sum_bij (fun ⟨i, j⟩ _ ↦ (j, i - j))
-- 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) :
        ℕ × ℕ)
⊢ 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₁ : (_ : ℕ) × ℕ)
  (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₂
Tactic: apply sum_bij (fun ⟨i, j⟩ _ ↦ (j, i - j))
-- 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₂
⊢ 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₂ : ∀ 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
Tactic: apply sum_bij (fun ⟨i, j⟩ _ ↦ (j, i - j))