awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
rw : smeval (ascPochhammer ℕ n) r = smeval (ascPochhammer R n) r
⊢ smeval (ascPochhammer ℕ n) r = eval r (ascPochhammer R n)
have rw₁ : smeval (ascPochhammer ℕ n) r = smeval (ascPochhammer ℕ n) r
Tactic: rw [eval_eq_smeval, ascPochhammer_smeval_cast R]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
ih : smeval (descPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
⊢ smeval (descPochhammer ℤ (n + 1)) r = smeval (ascPochhammer ℕ (n + 1)) (r - (↑(n + 1) : R) + 1)
have succ : smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1) *
    (smeval (R := ℤ) X r - HSMul.hSMul (α := ℤ) (↑n : ℤ) (HPow.hPow (β := ℕ) r 0)) =
  smeval (ascPochhammer ℕ n)
      (smeval (R := ℕ) X (r - (↑n : R)) + HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) (r - (↑n : R)) 0)) *
    (r - (↑n : R))
Tactic: rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, smeval_mul, ih,
      ascPochhammer_succ_left, X_mul, smeval_mul_X, smeval_comp, smeval_sub, ← C_eq_natCast,
      smeval_add, smeval_one, smeval_C]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
⊢ smeval (descPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
have zero : smeval (descPochhammer ℤ 0) r = smeval (ascPochhammer ℕ 0) (r - (↑0 : R) + 1)
Tactic: induction n with
  | zero => simp only [descPochhammer_zero, ascPochhammer_zero, smeval_one, npow_zero]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, smeval_mul, ih,
      ascPochhammer_succ_left, X_mul, smeval_mul_X, smeval_comp, smeval_sub, ← C_eq_natCast,
      smeval_add, smeval_one, smeval_C]
    simp only [smeval_X, npow_one, npow_zero, zsmul_one, Int.cast_natCast, one_smul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
zero : smeval (descPochhammer ℤ 0) r = smeval (ascPochhammer ℕ 0) (r - (↑0 : R) + 1)
⊢ smeval (descPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
have succ : ∀ (n : ℕ) (ih : smeval (descPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)),
  smeval (descPochhammer ℤ (n + 1)) r = smeval (ascPochhammer ℕ (n + 1)) (r - (↑(n + 1) : R) + 1)
Tactic: induction n with
  | zero => simp only [descPochhammer_zero, ascPochhammer_zero, smeval_one, npow_zero]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, smeval_mul, ih,
      ascPochhammer_succ_left, X_mul, smeval_mul_X, smeval_comp, smeval_sub, ← C_eq_natCast,
      smeval_add, smeval_one, smeval_C]
    simp only [smeval_X, npow_one, npow_zero, zsmul_one, Int.cast_natCast, one_smul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)
have zero : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑(n.descFactorial 0) : R)
Tactic: rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑(n.descFactorial 0) : R)
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)
have zero₁ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑1 : R)
Tactic: rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑(n.descFactorial 0) : R)
zero₁ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑1 : R)
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)
have zero₂ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) 1
Tactic: rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑(n.descFactorial 0) : R)
zero₁ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑1 : R)
zero₂ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) 1
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)
have zero₃ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (α := R) (β := ℕ) (↑n : R) 0) = 1
Tactic: rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑(n.descFactorial 0) : R)
zero₁ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑1 : R)
zero₂ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) 1
zero₃ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (α := R) (β := ℕ) (↑n : R) 0) = 1
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)
have zero₄ : HSMul.hSMul (α := ℕ) (β := R) 1 1 = 1
Tactic: rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑(n.descFactorial 0) : R)
zero₁ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑1 : R)
zero₂ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) 1
zero₃ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (α := R) (β := ℕ) (↑n : R) 0) = 1
zero₄ : HSMul.hSMul (α := ℕ) (β := R) 1 1 = 1
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)
have zero₅ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ (k + 1)) (↑n : R)) (↑(n.descFactorial (k + 1)) : R)
have succ : (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
  HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
Tactic: rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul,
      smeval_sub, smeval_X, smeval_natCast, npow_one, npow_zero, nsmul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
⊢ (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
have pos : ∀ (h : n < k),
  (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
Tactic: by_cases! h : n < k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
pos :
  ∀ (h : n < k),
    (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
      HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
⊢ (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
have neg : ∀ (h : k ≤ n),
  (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
Tactic: by_cases! h : n < k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
h : k ≤ n
⊢ (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
have neg : (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
  (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R)
Tactic: rw [Nat.cast_sub h]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
have zero : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)
Tactic: induction k with
  | zero =>
    rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
  | succ k ih =>
    rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul,
      smeval_sub, smeval_X, smeval_natCast, npow_one, npow_zero, nsmul_one]
    by_cases! h : n < k
    · simp only [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, zero_mul]
    · rw [Nat.cast_sub h]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
zero : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
have succ : ∀ (k : ℕ) (ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)),
  Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ (k + 1)) (↑n : R)) (↑(n.descFactorial (k + 1)) : R)
Tactic: induction k with
  | zero =>
    rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
  | succ k ih =>
    rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul,
      smeval_sub, smeval_X, smeval_natCast, npow_one, npow_zero, nsmul_one]
    by_cases! h : n < k
    · simp only [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, zero_mul]
    · rw [Nat.cast_sub h]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
⊢ smeval (ascPochhammer ℕ (k + 1)) (-r) = Int.negOnePow (↑(k + 1) : ℤ) • smeval (descPochhammer ℤ (k + 1)) r
have succ : Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
  Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
Tactic: simp only [ascPochhammer_succ_right, smeval_mul, ih, descPochhammer_succ_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (hypothesis)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
Tactic: have h : (X + (k : ℕ[X])).smeval (-r) = -(X + (-k : ℤ[X])).smeval r := by
      simp [smeval_natCast, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have succ : Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
  Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
Tactic: rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
succ :
  Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have succ₁ : -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
  Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
Tactic: rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
succ :
  Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₁ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have succ₂ : -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
  (HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)).negOnePow •
    (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
Tactic: rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
succ :
  Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₁ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₂ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have succ₃ : -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
  (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1).negOnePow •
    (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
Tactic: rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
succ :
  Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₁ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₂ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₃ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have succ₄ : -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
  -Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
Tactic: rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
succ :
  Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₁ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₂ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₃ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₄ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have succ₅ : -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
  -(Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
Tactic: rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]