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
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))
    (∑ 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 + 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))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
h : N + 1 ≤ i.1
⊢ HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * b ^ i.2) = 0
have inl : HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (0 * b ^ i.2) = 0
Tactic: rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
-- 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))
    (∑ 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 + 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))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
h : N + 1 ≤ i.1
inl : HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (0 * b ^ i.2) = 0
⊢ HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * b ^ i.2) = 0
have inl₁ : HSMul.hSMul (β := A) (HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹) 0 = 0
Tactic: rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
-- 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))
    (∑ 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 + 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))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
h : N + 1 ≤ i.1
inl : HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (0 * b ^ i.2) = 0
inl₁ : HSMul.hSMul (β := A) (HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹) 0 = 0
⊢ HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * b ^ i.2) = 0
have inl₂ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
-- 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))
    (∑ 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 + 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))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
h : i.1 < N + 1
⊢ HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * b ^ i.2) = 0
have inr : HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * 0) = 0
Tactic: rw [pow_eq_zero_of_le (hi.2 (Nat.le_of_lt_succ h)) h₅, mul_zero, smul_zero]
-- 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))
    (∑ 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 + 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))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
h : i.1 < N + 1
inr : HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * 0) = 0
⊢ HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * b ^ i.2) = 0
have inr₁ : HSMul.hSMul (β := A) (HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹) 0 = 0
Tactic: rw [pow_eq_zero_of_le (hi.2 (Nat.le_of_lt_succ h)) h₅, mul_zero, smul_zero]
-- 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))
    (∑ 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 + 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))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
h : i.1 < N + 1
inr : HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * 0) = 0
inr₁ : HSMul.hSMul (β := A) (HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹) 0 = 0
⊢ HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * b ^ i.2) = 0
have inr₂ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [pow_eq_zero_of_le (hi.2 (Nat.le_of_lt_succ h)) h₅, mul_zero, smul_zero]
-- 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)
s₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ 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 + 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))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
⊢ HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * b ^ i.2) = 0
have x : N + 1 ≤ i.1 ∨ i.1 < N + 1
Tactic: cases le_or_gt (N + 1) i.1 with
      | inl h => rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
      | inr h => rw [pow_eq_zero_of_le (hi.2 (Nat.le_of_lt_succ h)) h₅, mul_zero, smul_zero]
-- 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)
s₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ 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 + 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))
⊢ ∑ 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 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
Tactic: have z₂ : ∑ ij ∈ R2N ×ˢ R2N with ¬ (ij.1 ≤ N ∧ ij.2 ≤ N),
      ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0 :=
    sum_eq_zero fun i hi ↦ by
    simp only [not_and, not_le, mem_filter] at hi
    cases le_or_gt (N + 1) i.1 with
      | inl h => rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
      | inr h => rw [pow_eq_zero_of_le (hi.2 (Nat.le_of_lt_succ h)) h₅, mul_zero, smul_zero]
-- 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)
s₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ 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 + 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
⊢ ∑ 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 split₂ : HAdd.hAdd (α := 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 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)
Tactic: have split₂ := sum_filter_add_sum_filter_not (R2N ×ˢ R2N)
    (fun ij ↦ ij.1 ≤ N ∧ ij.2 ≤ N)
    (fun ij ↦ ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2))
-- 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)
s₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ 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 + 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₂ :
  HAdd.hAdd (α := 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 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)
⊢ ∑ 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 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))
Tactic: rw [z₂, add_zero] at split₂
Cleared hypotheses: split₂
-- 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)
s₁ :
  Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
    (∑ 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 + 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))
⊢ ∑ 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 s₂ : Eq.{u_1 + 1} (α := A) (∑ i ∈ R2N, HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i))
  (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
Tactic: rw [← split₂] at s₁
Cleared hypotheses: s₁, z₁, split₁, z₂, split₂
-- 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))
    (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.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))
⊢ 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))
have h : {ij ∈ R2N ×ˢ R2N | ij.1 ≤ N ∧ ij.2 ≤ N} = RN ×ˢ RN
Tactic: apply sum_congr
-- 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))
    (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.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))
h : {ij ∈ R2N ×ˢ R2N | ij.1 ≤ N ∧ ij.2 ≤ N} = RN ×ˢ RN
⊢ 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))
have a₁ : ∀ x ∈ RN ×ˢ RN,
  HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2) =
    HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2)
Tactic: apply sum_congr
-- 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))
    (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.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))
⊢ {ij ∈ R2N ×ˢ R2N | ij.1 ≤ N ∧ ij.2 ≤ N} = RN ×ˢ RN
have h : ∀ (x : ℕ × ℕ), x ∈ {ij ∈ R2N ×ˢ R2N | ij.1 ≤ N ∧ ij.2 ≤ N} ↔ x ∈ RN ×ˢ RN
Tactic: ext x
-- 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))
    (∑ x ∈ R2N ×ˢ R2N with x.1 ≤ N ∧ x.2 ≤ N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.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))
x : ℕ × ℕ
⊢ x ∈ {ij ∈ R2N ×ˢ R2N | ij.1 ≤ N ∧ ij.2 ≤ N} ↔ x ∈ RN ×ˢ RN
have h : (x.1 < 2 * N + 1 ∧ x.2 < 2 * N + 1) ∧ x.1 ≤ N ∧ x.2 ≤ N ↔ x.1 < N + 1 ∧ x.2 < N + 1
Tactic: simp only [mem_filter, mem_product, mem_range, hR2N, hRN]