awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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:
?_
-- 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)
⊢ 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:
?_
-- 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)
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)))
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))
⊢ 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))

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) := ?_

Premises used: HAdd.hAdd
-- 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)
⊢ 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:
sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- 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)
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))
⊢ 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:
refine sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- 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)
i : ℕ
h : i ∈ R2N
calc_1 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))
⊢ HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ ((a + b) ^ i) =
    HSMul.hSMul (α := ℚ) (β := A) (↑i ! : ℚ)⁻¹ (∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * (↑(i.choose j) : A))

Tactic:
rw [Commute.add_pow h₁ i]

Premises used: Commute.add_pow
-- 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)
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)))
⊢ 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:
simp_rw [smul_sum]

Premises used: Finset.smul_sum
-- 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)
⊢ 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:
sum_congr rfl fun i hi ↦ sum_congr rfl fun j hj ↦ ?_

Premises used: Finset.sum_congr, rfl
-- 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)
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))
⊢ 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:
refine sum_congr rfl fun i hi ↦ sum_congr rfl fun j hj ↦ ?_

Premises used: Finset.sum_congr, rfl
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ∈ range (i + 1)
⊢ j < i + 1

Tactic:
simp only [mem_range] at hi hj

Premises used: Finset.mem_range
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j < i + 1
⊢ j ≤ i

Tactic:
replace hj := Nat.le_of_lt_succ hj
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : HMul.hMul (α := ℚ) (↑i ! : ℚ)⁻¹ (↑(i.choose j) : ℚ) = HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹
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)))
⊢ HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j) * (↑(i.choose j) : A)) =
    HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹ • (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]

Premises used: Nat.choose, smul_assoc, nsmul_eq_mul, mul_smul_comm, SMulCommClass.smul_comm, SemigroupAction.mul_smul, Nat.cast_commute
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
this : HMul.hMul (α := ℚ) (↑i ! : ℚ)⁻¹ (↑(i.choose j) : ℚ) = HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  i.choose j • HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (i - j)) =
    i.choose j • HSMul.hSMul (α := ℚ) (↑i ! : ℚ)⁻¹ (a ^ j * b ^ (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)))

Tactic:
norm_cast
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
calc_2 : 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))

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
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ Ne (α := ℚ) (↑(j ! * (i - j)!) : ℚ) 0

Tactic:
positivity
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
calc_2 :
  (↑i ! : ℚ)⁻¹ * HDiv.hDiv (α := ℚ) (↑i ! : ℚ) (↑(j ! * (i - j)!) : ℚ) =
    HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹
⊢ HMul.hMul (α := ℚ) (↑i ! : ℚ)⁻¹ (↑(i.choose 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)]

Premises used: Nat.factorial_mul_factorial_dvd_factorial, Nat.cast_div, Nat.choose_eq_factorial_div_factorial
-- 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)
i : ℕ
hi : i ∈ R2N
j : ℕ
hj : j ≤ i
⊢ (↑i ! : ℚ)⁻¹ * HDiv.hDiv (α := ℚ) (↑i ! : ℚ) (↑(j ! * (i - j)!) : ℚ) =
    HMul.hMul (α := ℚ) (↑j ! : ℚ)⁻¹ (↑(i - j)! : ℚ)⁻¹

Tactic:
simp [field]
-- 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)
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))
⊢ 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:
rw [hR2N, sum_sigma']

Premises used: Finset.sum_sigma'
-- 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)
calc_3 :
  ∀ (a : (_ : ℕ) × ℕ),
    a.fst (β := fun (i : ℕ) ↦ ℕ) < 2 * N + 1 →
      a.snd (β := fun (i : ℕ) ↦ ℕ) < a.fst (β := fun (i : ℕ) ↦ ℕ) + 1 →
        (a.snd (β := fun (i : ℕ) ↦ ℕ) < 2 * N + 1 ∧
            a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ) < 2 * N + 1) ∧
          a.snd (β := fun (i : ℕ) ↦ ℕ) + (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) ≤ 2 * N
⊢ ∀ (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:
simp only [mem_sigma, mem_range, mem_filter, mem_product, and_imp]

Premises used: and_imp, Finset.mem_sigma, Finset.mem_range, Finset.mem_filter, Finset.mem_product
-- 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)
⊢ ∀ (a : (_ : ℕ) × ℕ),
    a.fst (β := fun (i : ℕ) ↦ ℕ) < 2 * N + 1 →
      a.snd (β := fun (i : ℕ) ↦ ℕ) < a.fst (β := fun (i : ℕ) ↦ ℕ) + 1 →
        (a.snd (β := fun (i : ℕ) ↦ ℕ) < 2 * N + 1 ∧
            a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ) < 2 * N + 1) ∧
          a.snd (β := fun (i : ℕ) ↦ ℕ) + (a.fst (β := fun (i : ℕ) ↦ ℕ) - a.snd (β := fun (i : ℕ) ↦ ℕ)) ≤ 2 * N

Tactic:
lia
-- 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)
calc_3 :
  ∀ (a₁ : (_ : ℕ) × ℕ),
    a₁.fst (β := fun (i : ℕ) ↦ ℕ) < 2 * N + 1 →
      a₁.snd (β := fun (i : ℕ) ↦ ℕ) < a₁.fst (β := fun (i : ℕ) ↦ ℕ) + 1 →
        ∀ (a₂ : (_ : ℕ) × ℕ),
          a₂.fst (β := fun (i : ℕ) ↦ ℕ) < 2 * N + 1 →
            a₂.snd (β := fun (i : ℕ) ↦ ℕ) < a₂.fst (β := fun (i : ℕ) ↦ ℕ) + 1 →
              a₁.snd (β := fun (i : ℕ) ↦ ℕ) = a₂.snd (β := fun (i : ℕ) ↦ ℕ) →
                a₁.fst (β := fun (i : ℕ) ↦ ℕ) - a₁.snd (β := fun (i : ℕ) ↦ ℕ) =
                    a₂.fst (β := fun (i : ℕ) ↦ ℕ) - a₂.snd (β := fun (i : ℕ) ↦ ℕ) →
                  a₁ = a₂
⊢ ∀ (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:
simp only [mem_sigma, mem_range, Prod.mk.injEq, and_imp]

Premises used: and_imp, Finset.mem_sigma, Finset.mem_range, Prod.mk.injEq
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁_1 : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄_1 : 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)
x₁ y₁ : ℕ
h₁ :
  Sigma.snd (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₁ y₁) <
    Sigma.fst (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₁ y₁) + 1
x₂ y₂ : ℕ
h₂ :
  Sigma.snd (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₂ y₂) <
    Sigma.fst (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₂ y₂) + 1
h₃ :
  Eq (α := ℕ) (Sigma.snd (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₁ y₁) : ℕ)
    (Sigma.snd (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₂ y₂) : ℕ)
h₄ :
  HSub.hSub (β := ℕ) (Sigma.fst (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₁ y₁))
      (Sigma.snd (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₁ y₁) : ℕ) =
    HSub.hSub (β := ℕ) (Sigma.fst (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₂ y₂))
      (Sigma.snd (β := fun (i : ℕ) ↦ ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₂ y₂) : ℕ)
calc_3 : ∀ (h₁ : y₂ ≤ x₁) (h₂ : y₂ ≤ x₂) (h₃ : y₁ = y₂) (h₄ : x₁ - y₂ = x₂ - y₂), x₁ = x₂
⊢ Eq (α := (_ : ℕ) × ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₁ y₁) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₂ y₂)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Nilpotent.Exp
Goal:
A : Type u_1
inst : Ring A
inst_1 : Module ℚ A
a b : A
h₁_1 : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄_1 : 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)
x₁ y₁ x₂ y₂ : ℕ
h₁ : y₂ ≤ x₁
h₂ : y₂ ≤ x₂
h₃ : y₁ = y₂
h₄ : x₁ - y₂ = x₂ - y₂
⊢ x₁ = x₂

Tactic:
lia
-- 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)
calc_3 :
  ∀ (a b : ℕ),
    a < 2 * N + 1 →
      b < 2 * N + 1 → a + b ≤ 2 * N → ∃ (a_4 : ℕ) (b_1 : ℕ), (a_4 < 2 * N + 1 ∧ b_1 < a_4 + 1) ∧ b_1 = a ∧ a_4 - b_1 = b
⊢ ∀ 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:
simp only [mem_filter, mem_product, mem_range, mem_sigma, exists_prop, Sigma.exists,
          and_imp, Prod.forall, Prod.mk.injEq]

Premises used: Sigma.exists, and_imp, Finset.mem_sigma, Finset.mem_range, exists_prop, Prod.mk.injEq, Prod.forall, Finset.mem_filter, Finset.mem_product
-- 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)
x y : ℕ
h : x < 2 * N + 1
h_1 : y < 2 * N + 1
h_2 : x + y ≤ 2 * N
⊢ (x + y < 2 * N + 1 ∧ x < x + y + 1) ∧ x = x ∧ x + y - x = y

Tactic:
lia
-- 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)
⊢ ∀ (a b : ℕ),
    a < 2 * N + 1 →
      b < 2 * N + 1 → a + b ≤ 2 * N → ∃ (a_4 : ℕ) (b_1 : ℕ), (a_4 < 2 * N + 1 ∧ b_1 < a_4 + 1) ∧ b_1 = a ∧ a_4 - b_1 = b

Tactic:
exact fun x y _ _ _ ↦ ⟨x + y, x, by lia⟩