awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
    (k + 1).factorial • multichoose (r + 1) k + smeval (ascPochhammer ℕ (k + 1)) r
have nth_rw : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X]) * ascPochhammer ℕ k).smeval (r + 1) =
  (k + 1).factorial • multichoose (r + 1) k +
    (X * Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval r
Tactic: nth_rw 1 [ascPochhammer_succ_right, ascPochhammer_succ_left, mul_comm (ascPochhammer ℕ k)]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X]) * ascPochhammer ℕ k).smeval (r + 1) =
    (k + 1).factorial • multichoose (r + 1) k +
      (X * Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval r
have simp : (HPow.hPow (β := ℕ) (r + 1) 1 + smeval (R := ℕ) (↑k : ℕ[X]) (r + 1)) * smeval (ascPochhammer ℕ k) (r + 1) =
  (k + 1).factorial • multichoose (r + 1) k +
    HPow.hPow (β := ℕ) r 1 * smeval (ascPochhammer ℕ k) (HPow.hPow (β := ℕ) r 1 + smeval (R := ℕ) 1 r)
Tactic: simp only [smeval_mul, smeval_comp, smeval_add, smeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ (HPow.hPow (β := ℕ) (r + 1) 1 + smeval (R := ℕ) (↑k : ℕ[X]) (r + 1)) * smeval (ascPochhammer ℕ k) (r + 1) =
    (k + 1).factorial • multichoose (r + 1) k +
      HPow.hPow (β := ℕ) r 1 * smeval (ascPochhammer ℕ k) (HPow.hPow (β := ℕ) r 1 + smeval (R := ℕ) 1 r)
have rw : (HPow.hPow (β := ℕ) (r + 1) 1 + smeval (R := ℕ) (↑k : ℕ[X]) (r + 1)) * smeval (ascPochhammer ℕ k) (r + 1) =
  k.succ • smeval (ascPochhammer ℕ k) (r + 1) +
    HPow.hPow (β := ℕ) r 1 * smeval (ascPochhammer ℕ k) (HPow.hPow (β := ℕ) r 1 + smeval (R := ℕ) 1 r)
Tactic: rw [Nat.factorial, mul_smul, factorial_nsmul_multichoose_eq_ascPochhammer]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ (HPow.hPow (β := ℕ) (r + 1) 1 + smeval (R := ℕ) (↑k : ℕ[X]) (r + 1)) * smeval (ascPochhammer ℕ k) (r + 1) =
    k.succ • smeval (ascPochhammer ℕ k) (r + 1) +
      HPow.hPow (β := ℕ) r 1 * smeval (ascPochhammer ℕ k) (HPow.hPow (β := ℕ) r 1 + smeval (R := ℕ) 1 r)
have simp : (r + 1 + smeval (R := ℕ) (↑k : ℕ[X]) (r + 1)) * smeval (ascPochhammer ℕ k) (r + 1) =
  k.succ • smeval (ascPochhammer ℕ k) (r + 1) + r * smeval (ascPochhammer ℕ k) (r + 1)
Tactic: simp only [smeval_one, npow_one, npow_zero, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ (r + 1 + smeval (R := ℕ) (↑k : ℕ[X]) (r + 1)) * smeval (ascPochhammer ℕ k) (r + 1) =
    k.succ • smeval (ascPochhammer ℕ k) (r + 1) + r * smeval (ascPochhammer ℕ k) (r + 1)
have rw : r * smeval (ascPochhammer ℕ k) (r + 1) +
    ((↑(↑k : ℕ) : R) * smeval (ascPochhammer ℕ k) (r + 1) + 1 * smeval (ascPochhammer ℕ k) (r + 1)) =
  k.succ • smeval (ascPochhammer ℕ k) (r + 1) + r * smeval (ascPochhammer ℕ k) (r + 1)
Tactic: rw [← C_eq_natCast, smeval_C, npow_zero, add_assoc, add_mul, add_comm 1, @nsmul_one, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ r * smeval (ascPochhammer ℕ k) (r + 1) +
      ((↑(↑k : ℕ) : R) * smeval (ascPochhammer ℕ k) (r + 1) + 1 * smeval (ascPochhammer ℕ k) (r + 1)) =
    k.succ • smeval (ascPochhammer ℕ k) (r + 1) + r * smeval (ascPochhammer ℕ k) (r + 1)
have rw : HSMul.hSMul (α := ℕ) (↑k : ℕ) (smeval (ascPochhammer ℕ k) (r + 1)) +
    (1 * smeval (ascPochhammer ℕ k) (r + 1) + r * smeval (ascPochhammer ℕ k) (r + 1)) =
  k • smeval (ascPochhammer ℕ k) (r + 1) + (smeval (ascPochhammer ℕ k) (r + 1) + r * smeval (ascPochhammer ℕ k) (r + 1))
Tactic: rw [← @nsmul_eq_mul, @add_rotate', @succ_nsmul, add_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ multichoose (r + 1) (k + 1) = multichoose r (k + 1) + multichoose (r + 1) k
have rw : (k + 1).factorial • multichoose (r + 1) (k + 1) = (k + 1).factorial • (multichoose r (k + 1) + multichoose (r + 1) k)
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ (k + 1).factorial • multichoose (r + 1) (k + 1) = (k + 1).factorial • (multichoose r (k + 1) + multichoose (r + 1) k)
have simp : smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
  smeval (ascPochhammer ℕ (k + 1)) r + (k + 1).factorial • multichoose (r + 1) k
Tactic: simp only [factorial_nsmul_multichoose_eq_ascPochhammer, smul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
    smeval (ascPochhammer ℕ (k + 1)) r + (k + 1).factorial • multichoose (r + 1) k
have rw : smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
  (k + 1).factorial • multichoose (r + 1) k + smeval (ascPochhammer ℕ (k + 1)) r
Tactic: rw [add_comm (smeval (ascPochhammer ℕ (k + 1)) r), ascPochhammer_succ_succ r k]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
rw :
  smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
    (k + 1).factorial • multichoose (r + 1) k + smeval (ascPochhammer ℕ (k + 1)) r
⊢ smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
    smeval (ascPochhammer ℕ (k + 1)) r + (k + 1).factorial • multichoose (r + 1) k
have rw₁ : (k + 1).factorial • multichoose (r + 1) k + smeval (ascPochhammer ℕ (k + 1)) r =
  (k + 1).factorial • multichoose (r + 1) k + smeval (ascPochhammer ℕ (k + 1)) r
Tactic: rw [add_comm (smeval (ascPochhammer ℕ (k + 1)) r), ascPochhammer_succ_succ r k]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : Eq.{u_2 + 1} (α := R) (multichoose 1 n) 1
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 (n + 1)) 1
have succ : multichoose (HAdd.hAdd (α := R) 0 1) (n + 1) = HAdd.hAdd (α := R) 0 1
Tactic: rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
      multichoose_zero_succ, zero_add, zero_add, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : Eq.{u_2 + 1} (α := R) (multichoose 1 n) 1
succ : multichoose (HAdd.hAdd (α := R) 0 1) (n + 1) = HAdd.hAdd (α := R) 0 1
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 (n + 1)) 1
have succ₁ : multichoose 0 (n + 1) + multichoose (HAdd.hAdd (α := R) 0 1) n = HAdd.hAdd (α := R) 0 1
Tactic: rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
      multichoose_zero_succ, zero_add, zero_add, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : Eq.{u_2 + 1} (α := R) (multichoose 1 n) 1
succ : multichoose (HAdd.hAdd (α := R) 0 1) (n + 1) = HAdd.hAdd (α := R) 0 1
succ₁ : multichoose 0 (n + 1) + multichoose (HAdd.hAdd (α := R) 0 1) n = HAdd.hAdd (α := R) 0 1
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 (n + 1)) 1
have succ₂ : 0 + multichoose (HAdd.hAdd (α := R) 0 1) n = HAdd.hAdd (α := R) 0 1
Tactic: rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
      multichoose_zero_succ, zero_add, zero_add, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : Eq.{u_2 + 1} (α := R) (multichoose 1 n) 1
succ : multichoose (HAdd.hAdd (α := R) 0 1) (n + 1) = HAdd.hAdd (α := R) 0 1
succ₁ : multichoose 0 (n + 1) + multichoose (HAdd.hAdd (α := R) 0 1) n = HAdd.hAdd (α := R) 0 1
succ₂ : 0 + multichoose (HAdd.hAdd (α := R) 0 1) n = HAdd.hAdd (α := R) 0 1
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 (n + 1)) 1
have succ₃ : multichoose (HAdd.hAdd (α := R) 0 1) n = HAdd.hAdd (α := R) 0 1
Tactic: rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
      multichoose_zero_succ, zero_add, zero_add, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : Eq.{u_2 + 1} (α := R) (multichoose 1 n) 1
succ : multichoose (HAdd.hAdd (α := R) 0 1) (n + 1) = HAdd.hAdd (α := R) 0 1
succ₁ : multichoose 0 (n + 1) + multichoose (HAdd.hAdd (α := R) 0 1) n = HAdd.hAdd (α := R) 0 1
succ₂ : 0 + multichoose (HAdd.hAdd (α := R) 0 1) n = HAdd.hAdd (α := R) 0 1
succ₃ : multichoose (HAdd.hAdd (α := R) 0 1) n = HAdd.hAdd (α := R) 0 1
succ₄ : Eq.{u_2 + 1} (α := R) (multichoose 1 n) 1
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 (n + 1)) 1
have succ₅ : Eq.{u_2 + 1} (α := R) 1 1
Tactic: rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
      multichoose_zero_succ, zero_add, zero_add, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 k) 1
have zero : Eq.{u_2 + 1} (α := R) (multichoose 1 0) 1
Tactic: induction k with
  | zero => exact multichoose_zero_right 1
  | succ n ih =>
    rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
      multichoose_zero_succ, zero_add, zero_add, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
zero : Eq.{u_2 + 1} (α := R) (multichoose 1 0) 1
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 k) 1
have succ : ∀ (n : ℕ) (ih : Eq.{u_2 + 1} (α := R) (multichoose 1 n) 1), Eq.{u_2 + 1} (α := R) (multichoose 1 (n + 1)) 1
Tactic: induction k with
  | zero => exact multichoose_zero_right 1
  | succ n ih =>
    rw [show (1 : R) = 0 + 1 by exact (@zero_add R _ 1).symm, multichoose_succ_succ,
      multichoose_zero_succ, zero_add, zero_add, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
⊢ multichoose 2 0 = HAdd.hAdd (α := R) (↑0 : R) 1
have zero : 1 = HAdd.hAdd (α := R) (↑0 : R) 1
Tactic: rw [multichoose_zero_right, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
zero : 1 = HAdd.hAdd (α := R) (↑0 : R) 1
⊢ multichoose 2 0 = HAdd.hAdd (α := R) (↑0 : R) 1
have zero₁ : 1 = HAdd.hAdd (α := R) 0 1
Tactic: rw [multichoose_zero_right, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
zero : 1 = HAdd.hAdd (α := R) (↑0 : R) 1
zero₁ : 1 = HAdd.hAdd (α := R) 0 1
⊢ multichoose 2 0 = HAdd.hAdd (α := R) (↑0 : R) 1
have zero₂ : Eq.{u_2 + 1} (α := R) 1 1
Tactic: rw [multichoose_zero_right, Nat.cast_zero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : multichoose 2 n = HAdd.hAdd (α := R) (↑n : R) 1
⊢ multichoose 2 (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
have succ : multichoose (HAdd.hAdd (α := R) 1 1) (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
Tactic: rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : multichoose 2 n = HAdd.hAdd (α := R) (↑n : R) 1
succ : multichoose (HAdd.hAdd (α := R) 1 1) (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
⊢ multichoose 2 (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
have succ₁ : multichoose 1 (n + 1) + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
Tactic: rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : multichoose 2 n = HAdd.hAdd (α := R) (↑n : R) 1
succ : multichoose (HAdd.hAdd (α := R) 1 1) (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₁ : multichoose 1 (n + 1) + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
⊢ multichoose 2 (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
have succ₂ : 1 + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
Tactic: rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : multichoose 2 n = HAdd.hAdd (α := R) (↑n : R) 1
succ : multichoose (HAdd.hAdd (α := R) 1 1) (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₁ : multichoose 1 (n + 1) + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₂ : 1 + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
⊢ multichoose 2 (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
have succ₃ : HAdd.hAdd (α := R) 1 (multichoose 2 n) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
Tactic: rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : multichoose 2 n = HAdd.hAdd (α := R) (↑n : R) 1
succ : multichoose (HAdd.hAdd (α := R) 1 1) (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₁ : multichoose 1 (n + 1) + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₂ : 1 + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₃ : HAdd.hAdd (α := R) 1 (multichoose 2 n) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
⊢ multichoose 2 (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
have succ₄ : 1 + HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
Tactic: rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : multichoose 2 n = HAdd.hAdd (α := R) (↑n : R) 1
succ : multichoose (HAdd.hAdd (α := R) 1 1) (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₁ : multichoose 1 (n + 1) + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₂ : 1 + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₃ : HAdd.hAdd (α := R) 1 (multichoose 2 n) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₄ : 1 + HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
⊢ multichoose 2 (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
have succ₅ : 1 + HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑n : R) 1 + 1
Tactic: rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
n : ℕ
ih : multichoose 2 n = HAdd.hAdd (α := R) (↑n : R) 1
succ : multichoose (HAdd.hAdd (α := R) 1 1) (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₁ : multichoose 1 (n + 1) + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₂ : 1 + multichoose (HAdd.hAdd (α := R) 1 1) n = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₃ : HAdd.hAdd (α := R) 1 (multichoose 2 n) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₄ : 1 + HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
succ₅ : 1 + HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑n : R) 1 + 1
⊢ multichoose 2 (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
have succ₆ : HAdd.hAdd (α := R) (↑n : R) 1 + 1 = HAdd.hAdd (α := R) (↑n : R) 1 + 1
Tactic: rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
⊢ multichoose 2 k = HAdd.hAdd (α := R) (↑k : R) 1
have zero : multichoose 2 0 = HAdd.hAdd (α := R) (↑0 : R) 1
Tactic: induction k with
  | zero =>
    rw [multichoose_zero_right, Nat.cast_zero, zero_add]
  | succ n ih =>
    rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
zero : multichoose 2 0 = HAdd.hAdd (α := R) (↑0 : R) 1
⊢ multichoose 2 k = HAdd.hAdd (α := R) (↑k : R) 1
have succ : ∀ (n : ℕ) (ih : multichoose 2 n = HAdd.hAdd (α := R) (↑n : R) 1),
  multichoose 2 (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
Tactic: induction k with
  | zero =>
    rw [multichoose_zero_right, Nat.cast_zero, zero_add]
  | succ n ih =>
    rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
      Nat.cast_succ, add_comm]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : BinomialRing R
inst_3 : BinomialRing S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
f : F
a : R
n : ℕ
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (multichoose a n) : S) (multichoose ((f : (a : R) → S) a) n : S)
have a₁ : Eq.{u_4 + 1} (α := S) ((fun (a : S) ↦ n.factorial • a) ((f : (a : R) → S) (multichoose a n)))
  ((fun (a : S) ↦ n.factorial • a) (multichoose ((f : (a : R) → S) a) n))
Tactic: apply nsmul_right_injective n.factorial_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : BinomialRing R
inst_3 : BinomialRing S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
f : F
a : R
n : ℕ
⊢ Eq.{u_4 + 1} (α := S) ((fun (a : S) ↦ n.factorial • a) ((f : (a : R) → S) (multichoose a n)))
    ((fun (a : S) ↦ n.factorial • a) (multichoose ((f : (a : R) → S) a) n))
have a₁ : eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) RingHom.smulOneHom)
    (((↑f : R →+* S) : (a : R) → S) a) (ascPochhammer ℕ n) =
  eval₂ RingHom.smulOneHom (((↑f : R →+* S) : (a : R) → S) a) (ascPochhammer ℕ n)
Tactic: simp only [← map_nsmul, Ring.factorial_nsmul_multichoose_eq_ascPochhammer,
    ← Polynomial.eval₂_smulOneHom_eq_smeval, Polynomial.hom_eval₂, ← RingHom.coe_coe f]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_3
S : Type u_4
F : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : BinomialRing R
inst_3 : BinomialRing S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
f : F
a : R
n : ℕ
⊢ eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) RingHom.smulOneHom)
      (((↑f : R →+* S) : (a : R) → S) a) (ascPochhammer ℕ n) =
    eval₂ RingHom.smulOneHom (((↑f : R →+* S) : (a : R) → S) a) (ascPochhammer ℕ n)
have a₁ : Eq (α := ℕ →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) RingHom.smulOneHom)
  RingHom.smulOneHom
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Pow S ℕ
inst_3 : Module R S
inst_4 : IsScalarTower R S S
inst_5 : NatPowAssoc S
x : S
n : ℕ
hn : smeval (ascPochhammer R n) x = smeval (ascPochhammer ℕ n) x
⊢ smeval (ascPochhammer R (n + 1)) x = smeval (ascPochhammer ℕ (n + 1)) x
have succ : smeval (ascPochhammer R n) x * x + (HMul.hMul (α := R[X]) (↑n : R[X]) (ascPochhammer R n)).smeval x =
  smeval (ascPochhammer ℕ n) x * x + (HMul.hMul (α := ℕ[X]) (↑n : ℕ[X]) (ascPochhammer ℕ n)).smeval x
Tactic: simp only [ascPochhammer_succ_right, mul_add, smeval_add, smeval_mul_X, ← Nat.cast_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Pow S ℕ
inst_3 : Module R S
inst_4 : IsScalarTower R S S
inst_5 : NatPowAssoc S
x : S
n : ℕ
hn : smeval (ascPochhammer R n) x = smeval (ascPochhammer ℕ n) x
⊢ smeval (ascPochhammer R n) x * x + (HMul.hMul (α := R[X]) (↑n : R[X]) (ascPochhammer R n)).smeval x =
    smeval (ascPochhammer ℕ n) x * x + (HMul.hMul (α := ℕ[X]) (↑n : ℕ[X]) (ascPochhammer ℕ n)).smeval x
have succ : smeval (ascPochhammer ℕ n) x * x + n • smeval (ascPochhammer ℕ n) x =
  smeval (ascPochhammer ℕ n) x * x + HSMul.hSMul (α := ℕ) (↑n : ℕ) (smeval (ascPochhammer ℕ n) x)
Tactic: simp only [← C_eq_natCast, smeval_C_mul, hn, Nat.cast_smul_eq_nsmul R n]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Pow S ℕ
inst_3 : Module R S
inst_4 : IsScalarTower R S S
inst_5 : NatPowAssoc S
x : S
n : ℕ
⊢ smeval (ascPochhammer R n) x = smeval (ascPochhammer ℕ n) x
have zero : smeval (ascPochhammer R 0) x = smeval (ascPochhammer ℕ 0) x
Tactic: induction n with
  | zero => simp only [ascPochhammer_zero, smeval_one]
  | succ n hn =>
    simp only [ascPochhammer_succ_right, mul_add, smeval_add, smeval_mul_X, ← Nat.cast_comm]
    simp only [← C_eq_natCast, smeval_C_mul, hn, Nat.cast_smul_eq_nsmul R n]
    simp only [nsmul_eq_mul, Nat.cast_id]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Pow S ℕ
inst_3 : Module R S
inst_4 : IsScalarTower R S S
inst_5 : NatPowAssoc S
x : S
n : ℕ
zero : smeval (ascPochhammer R 0) x = smeval (ascPochhammer ℕ 0) x
⊢ smeval (ascPochhammer R n) x = smeval (ascPochhammer ℕ n) x
have succ : ∀ (n : ℕ) (hn : smeval (ascPochhammer R n) x = smeval (ascPochhammer ℕ n) x),
  smeval (ascPochhammer R (n + 1)) x = smeval (ascPochhammer ℕ (n + 1)) x
Tactic: induction n with
  | zero => simp only [ascPochhammer_zero, smeval_one]
  | succ n hn =>
    simp only [ascPochhammer_succ_right, mul_add, smeval_add, smeval_mul_X, ← Nat.cast_comm]
    simp only [← C_eq_natCast, smeval_C_mul, hn, Nat.cast_smul_eq_nsmul R n]
    simp only [nsmul_eq_mul, Nat.cast_id]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
⊢ smeval (ascPochhammer ℕ n) r = eval r (ascPochhammer R n)
have rw : smeval (ascPochhammer ℕ n) r = smeval (ascPochhammer R n) r
Tactic: rw [eval_eq_smeval, ascPochhammer_smeval_cast R]