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)
⊢ ∀ (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) :
        ℕ × ℕ)
have 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
Tactic: simp only [mem_sigma, mem_range, mem_filter, mem_product, and_imp]
-- 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)
⊢ ∀ (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₂
have 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₂
Tactic: simp only [mem_sigma, mem_range, Prod.mk.injEq, and_imp]
-- 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₁_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₂) : ℕ)
⊢ Eq (α := (_ : ℕ) × ℕ) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₁ y₁) (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) x₂ y₂)
have calc_3 : ∀ (h₁ : y₂ ≤ x₁) (h₂ : y₂ ≤ x₂) (h₃ : y₁ = y₂) (h₄ : x₁ - y₂ = x₂ - y₂), x₁ = x₂
Tactic: simp_all
Cleared hypotheses: h₁, h₂, h₃, 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
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
⊢ ∀ 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
have 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
Tactic: simp only [mem_filter, mem_product, mem_range, mem_sigma, exists_prop, Sigma.exists,
          and_imp, Prod.forall, Prod.mk.injEq]
-- 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 ∈ 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))
  (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
Tactic: have s₁ := by
    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) := ?_
    · refine sum_congr rfl fun i _ ↦ ?_
      rw [Commute.add_pow h₁ i]
    · simp_rw [smul_sum]
      refine sum_congr rfl fun i hi ↦ sum_congr rfl fun j hj ↦ ?_
      simp only [mem_range] at hi hj
      replace hj := Nat.le_of_lt_succ hj
      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
      rw [Nat.choose_eq_factorial_div_factorial hj,
        Nat.cast_div (Nat.factorial_mul_factorial_dvd_factorial hj) (by positivity)]
      simp [field]
    · rw [hR2N, sum_sigma']
      apply sum_bij (fun ⟨i, j⟩ _ ↦ (j, i - j))
      · simp only [mem_sigma, mem_range, mem_filter, mem_product, and_imp]
        lia
      · simp only [mem_sigma, mem_range, Prod.mk.injEq, and_imp]
        rintro ⟨x₁, y₁⟩ - h₁ ⟨x₂, y₂⟩ - h₂ h₃ h₄
        simp_all
        lia
      · simp only [mem_filter, mem_product, mem_range, mem_sigma, exists_prop, Sigma.exists,
          and_imp, Prod.forall, Prod.mk.injEq]
        exact fun x y _ _ _ ↦ ⟨x + y, x, by lia⟩
      · simp only [mem_sigma, mem_range, implies_true]
-- 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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
i : ℕ × ℕ
hi : i ∈ {ij ∈ R2N ×ˢ R2N | ¬ij.1 + ij.2 ≤ 2 * N}
⊢ HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * b ^ i.2) = 0
have hi₁ : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
Tactic: rw [mem_filter] at hi
Cleared hypotheses: hi
-- 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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
h : i.1 < N + 1
⊢ N + 1 ≤ i.2
have linarith : i.2 < N + 1 →
  -1 + (HMul.hMul (α := ℤ) 2 (↑N : ℤ) + 1 - HAdd.hAdd (α := ℤ) (↑i.1 : ℤ) (↑i.2 : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑i.1 : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) +
      (HAdd.hAdd (α := ℤ) (↑i.2 : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑N : ℤ) 1) =
    0
Tactic: linarith
-- 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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
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 (by linarith) 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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
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 (by linarith) 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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
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 (by linarith) 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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
i : ℕ × ℕ
hi : i ∈ R2N ×ˢ R2N ∧ ¬i.1 + i.2 ≤ 2 * N
⊢ 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 _ => rw [pow_eq_zero_of_le (by linarith) 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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.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 + ij.2 ≤ 2 * N,
    HMul.hMul (α := ℚ) (↑ij.1! : ℚ)⁻¹ (↑ij.2! : ℚ)⁻¹ • (a ^ ij.1 * b ^ ij.2))
  0
Tactic: have z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ ij.1 + ij.2 ≤ 2 * N,
      ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0 :=
    sum_eq_zero fun i hi ↦ by
      rw [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 _ => rw [pow_eq_zero_of_le (by linarith) 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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      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
⊢ ∑ 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 + x.2 ≤ 2 * N, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
    (∑ 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)
Tactic: have split₁ := sum_filter_add_sum_filter_not (R2N ×ˢ R2N)
    (fun ij ↦ ij.1 + ij.2 ≤ 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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      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₁ :
  HAdd.hAdd (α := 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 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 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))
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))
    (∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
      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))
⊢ ∑ 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, HMul.hMul (α := ℚ) (↑x.1! : ℚ)⁻¹ (↑x.2! : ℚ)⁻¹ • (a ^ x.1 * b ^ x.2))
Tactic: rw [split₁] at s₁
Cleared hypotheses: s₁, z₁, 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))
i : ℕ × ℕ
hi : i ∈ {ij ∈ R2N ×ˢ R2N | ¬(ij.1 ≤ N ∧ ij.2 ≤ N)}
⊢ HMul.hMul (α := ℚ) (↑i.1! : ℚ)⁻¹ (↑i.2! : ℚ)⁻¹ • (a ^ i.1 * b ^ i.2) = 0
have hi₁ : i ∈ R2N ×ˢ R2N ∧ (i.1 ≤ N → N < i.2)
Tactic: simp only [not_and, not_le, mem_filter] at hi
Cleared hypotheses: hi