awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Eq (α := (a : A ⊗[R] A) → A) (⇑(mulCoalgHom R A) : (a : A ⊗[R] A) → A) (⇑(LinearMap.mul' R A) : (a : A ⊗[R] A) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Bialgebra R A
⊢ Eq (α := A ⊗[R] A →ₐ[R] A) (↑(mulBialgHom R A) : A ⊗[R] A →ₐ[R] A) (Algebra.TensorProduct.lmul' R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.lmul', MonoidHomClass.toMonoidHom, BialgHom.toAlgHom, AlgHom.restrictScalars, RingHomClass.toRingHom, TensorProduct, rfl
-- Module: Mathlib.RingTheory.Bialgebra.TensorProduct
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Bialgebra R A
⊢ Eq (α := (a : A ⊗[R] A) → A) (⇑(mulBialgHom R A) : (a : A ⊗[R] A) → A) (⇑(LinearMap.mul' R A) : (a : A ⊗[R] A) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
n : ℕ
⊢ @BinomialRing.multichoose _ inst inst_1 _ r n = multichoose r n

Tactic:
rfl

Premises used: Ring.multichoose, rfl
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
n : ℕ
⊢ n.factorial • multichoose r n = smeval (ascPochhammer ℕ n) r

Tactic:
BinomialRing.factorial_nsmul_multichoose r n

Premises used: BinomialRing.factorial_nsmul_multichoose, Ring.multichoose
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 0 • multichoose r 0 = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₁ : smeval (ascPochhammer ℕ 0) r = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₂ : smeval (R := ℕ) 1 r = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₃ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0) = Nat.factorial 0 • HPow.hPow (β := ℕ) r 0
rw₄ rw₅ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0) = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0)
⊢ multichoose r 0 = HPow.hPow (β := ℕ) r 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero 0),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero, smeval_one, Nat.factorial]

Premises used: Ring.factorial_nsmul_multichoose_eq_ascPochhammer, Polynomial.smeval_one, ascPochhammer_zero, nsmul_right_inj, Nat.factorial_ne_zero, Nat.factorial, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : MulOneClass R
inst_4 : NatPowAssoc R
r : R
rw : HPow.hPow (β := ℕ) r 0 = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ multichoose r 0 = 1

Tactic:
rw [multichoose_zero_right', npow_zero]

Premises used: npow_zero, Ring.multichoose_zero_right'
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 1 • multichoose r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₁ : smeval (ascPochhammer ℕ 1) r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₂ : smeval (R := ℕ) X r = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₃ : HPow.hPow (β := ℕ) r 1 = Nat.factorial 1 • HPow.hPow (β := ℕ) r 1
rw₄ : HPow.hPow (β := ℕ) r 1 = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 1)
rw₅ rw₆ : HPow.hPow (β := ℕ) r 1 = HPow.hPow (β := ℕ) r 1
⊢ multichoose r 1 = HPow.hPow (β := ℕ) r 1

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero 1),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_one, smeval_X, Nat.factorial_one,
    one_smul]

Premises used: ascPochhammer_one, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, Polynomial.smeval_X, one_smul, nsmul_right_inj, Nat.factorial_ne_zero, OfNat.ofNat, Nat.factorial_one
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : MulOneClass R
inst_4 : NatPowAssoc R
r : R
rw : HPow.hPow (β := ℕ) r 1 = r
rw₁ rw₂ : r = r
⊢ multichoose r 1 = r

Tactic:
rw [multichoose_one_right', npow_one]

Premises used: npow_one, Ring.multichoose_one_right'
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
rw : HSMul.hSMul (β := R) (k + 1).factorial (multichoose 0 (k + 1)) = HSMul.hSMul (β := R) (k + 1).factorial 0
rw₁ : smeval (ascPochhammer ℕ (k + 1)) 0 = HSMul.hSMul (β := R) (k + 1).factorial 0
rw₂ : Eq.{u_2 + 1} (α := R) (smeval (ascPochhammer ℕ (k + 1)) 0) 0
rw₃ : Eq.{u_2 + 1} (α := R) ((X * Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval 0) 0
rw₄ : HMul.hMul (α := R) 0 ((Polynomial.comp (ascPochhammer ℕ k) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval 0) = 0
rw₅ rw₆ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) (multichoose 0 (k + 1)) 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero, ascPochhammer_succ_left,
    smeval_X_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, smul_zero, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, Polynomial.smeval_X_mul, nsmul_right_inj, Nat.factorial_ne_zero, HAdd.hAdd, OfNat.ofNat, ascPochhammer_succ_left
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
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
⊢ smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
    (k + 1).factorial • multichoose (r + 1) k + smeval (ascPochhammer ℕ (k + 1)) r

Tactic:
nth_rw 1 [ascPochhammer_succ_right, ascPochhammer_succ_left, mul_comm (ascPochhammer ℕ k)]

Premises used: ascPochhammer, Nat, mul_comm, ascPochhammer_succ_left, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
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)
⊢ (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:
simp only [smeval_mul, smeval_comp, smeval_add, smeval_X]

Premises used: Polynomial.smeval_mul, Polynomial.smeval_X, Polynomial.smeval_comp, Polynomial.smeval_add
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
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)
⊢ (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:
rw [Nat.factorial, mul_smul, factorial_nsmul_multichoose_eq_ascPochhammer]

Premises used: Ring.factorial_nsmul_multichoose_eq_ascPochhammer, Nat.factorial, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
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)
⊢ (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:
simp only [smeval_one, npow_one, npow_zero, one_smul]

Premises used: npow_one, npow_zero, one_smul, Polynomial.smeval_one
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
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)
⊢ (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:
rw [← C_eq_natCast, smeval_C, npow_zero, add_assoc, add_mul, add_comm 1, @nsmul_one, add_mul]

Premises used: add_mul, add_assoc, Polynomial.C_eq_natCast, Polynomial.smeval_C, npow_zero, add_comm, nsmul_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
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))
⊢ 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 [← @nsmul_eq_mul, @add_rotate', @succ_nsmul, add_assoc]

Premises used: add_assoc, add_rotate', nsmul_eq_mul, succ_nsmul
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
⊢ 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:
simp_all only [Nat.cast_id, nsmul_eq_mul, one_mul]

Premises used: Nat.cast_id, nsmul_eq_mul, one_mul
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
rw :
  (k + 1).factorial • multichoose (r + 1) (k + 1) = (k + 1).factorial • (multichoose r (k + 1) + multichoose (r + 1) k)
⊢ multichoose (r + 1) (k + 1) = multichoose r (k + 1) + multichoose (r + 1) k

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]

Premises used: nsmul_right_inj, Nat.factorial_ne_zero, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
r : R
k : ℕ
simp :
  smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
    smeval (ascPochhammer ℕ (k + 1)) r + (k + 1).factorial • multichoose (r + 1) k
⊢ (k + 1).factorial • multichoose (r + 1) (k + 1) = (k + 1).factorial • (multichoose r (k + 1) + multichoose (r + 1) k)

Tactic:
simp only [factorial_nsmul_multichoose_eq_ascPochhammer, smul_add]

Premises used: Ring.factorial_nsmul_multichoose_eq_ascPochhammer, smul_add
-- Module: Mathlib.RingTheory.Binomial
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
rw₁ 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
⊢ smeval (ascPochhammer ℕ (k + 1)) (r + 1) =
    smeval (ascPochhammer ℕ (k + 1)) r + (k + 1).factorial • multichoose (r + 1) k

Tactic:
rw [add_comm (smeval (ascPochhammer ℕ (k + 1)) r), ascPochhammer_succ_succ r k]

Premises used: ascPochhammer, add_comm, Ring.ascPochhammer_succ_succ, HAdd.hAdd, Nat, OfNat.ofNat, Polynomial.smeval
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 0) 1

Tactic:
multichoose_zero_right 1

Premises used: Ring.multichoose_zero_right, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 0) 1

Tactic:
exact multichoose_zero_right 1

Premises used: Ring.multichoose_zero_right, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
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
⊢ 1 = HAdd.hAdd (α := R) 0 1

Tactic:
(@zero_add R _ 1).symm

Premises used: zero_add, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Binomial
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
⊢ 1 = HAdd.hAdd (α := R) 0 1

Tactic:
exact (@zero_add R _ 1).symm

Premises used: zero_add, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Binomial
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
succ₅ succ₆ : Eq.{u_2 + 1} (α := R) 1 1
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 (n + 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]

Premises used: Ring.multichoose_zero_succ, zero_add, Ring.multichoose_succ_succ
-- Module: Mathlib.RingTheory.Binomial
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
succ : ∀ (n : ℕ) (ih : Eq.{u_2 + 1} (α := R) (multichoose 1 n) 1), Eq.{u_2 + 1} (α := R) (multichoose 1 (n + 1)) 1
⊢ Eq.{u_2 + 1} (α := R) (multichoose 1 k) 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]

Premises used: Ring.multichoose_zero_succ, Ring.multichoose_zero_right, zero_add, Ring.multichoose_succ_succ, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
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
zero₂ zero₃ : Eq.{u_2 + 1} (α := R) 1 1
⊢ multichoose 2 0 = HAdd.hAdd (α := R) (↑0 : R) 1

Tactic:
rw [multichoose_zero_right, Nat.cast_zero, zero_add]

Premises used: Ring.multichoose_zero_right, zero_add, Nat.cast_zero
-- Module: Mathlib.RingTheory.Binomial
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
succ₆ succ₇ : HAdd.hAdd (α := R) (↑n : R) 1 + 1 = HAdd.hAdd (α := R) (↑n : R) 1 + 1
⊢ multichoose 2 (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]

Premises used: Nat.cast_succ, one_add_one_eq_two, add_comm, Ring.multichoose_one, Ring.multichoose_succ_succ, Eq.symm
-- Module: Mathlib.RingTheory.Binomial
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
succ :
  ∀ (n : ℕ) (ih : multichoose 2 n = HAdd.hAdd (α := R) (↑n : R) 1),
    multichoose 2 (n + 1) = HAdd.hAdd (α := R) (↑(n + 1) : R) 1
⊢ multichoose 2 k = HAdd.hAdd (α := R) (↑k : 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]

Premises used: Nat.cast_succ, Ring.multichoose_zero_right, zero_add, one_add_one_eq_two, add_comm, Nat.cast_zero, Ring.multichoose_one, Ring.multichoose_succ_succ, Eq.symm
-- Module: Mathlib.RingTheory.Binomial
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 : ℕ
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))
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (multichoose a n) : S) (multichoose ((f : (a : R) → S) a) n : S)

Tactic:
apply nsmul_right_injective n.factorial_ne_zero

Premises used: Nat.factorial_ne_zero, nsmul_right_injective
-- Module: Mathlib.RingTheory.Binomial
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 : ℕ
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)
⊢ 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:
simp only [← map_nsmul, Ring.factorial_nsmul_multichoose_eq_ascPochhammer,
    ← Polynomial.eval₂_smulOneHom_eq_smeval, Polynomial.hom_eval₂, ← RingHom.coe_coe f]

Premises used: Polynomial.hom_eval₂, RingHom.coe_coe, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, map_nsmul, Polynomial.eval₂_smulOneHom_eq_smeval
-- Module: Mathlib.RingTheory.Binomial
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 : ℕ
a₁ :
  Eq (α := ℕ →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) RingHom.smulOneHom)
    RingHom.smulOneHom
⊢ 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:
congr
-- Module: Mathlib.RingTheory.Binomial
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 (α := ℕ →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) RingHom.smulOneHom)
    RingHom.smulOneHom

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Binomial
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 (α := ℕ →+* S) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) RingHom.smulOneHom)
    RingHom.smulOneHom

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Binomial
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
⊢ smeval (ascPochhammer R 0) x = smeval (ascPochhammer ℕ 0) x

Tactic:
simp only [ascPochhammer_zero, smeval_one]

Premises used: Polynomial.smeval_one, ascPochhammer_zero
-- Module: Mathlib.RingTheory.Binomial
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
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
⊢ smeval (ascPochhammer R (n + 1)) x = smeval (ascPochhammer ℕ (n + 1)) x

Tactic:
simp only [ascPochhammer_succ_right, mul_add, smeval_add, smeval_mul_X, ← Nat.cast_comm]

Premises used: Nat.cast_comm, Polynomial.smeval_mul_X, mul_add, Polynomial.smeval_add, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Binomial
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
succ :
  smeval (ascPochhammer ℕ n) x * x + n • smeval (ascPochhammer ℕ n) x =
    smeval (ascPochhammer ℕ n) x * x + HSMul.hSMul (α := ℕ) (↑n : ℕ) (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

Tactic:
simp only [← C_eq_natCast, smeval_C_mul, hn, Nat.cast_smul_eq_nsmul R n]

Premises used: Polynomial.C_eq_natCast, Polynomial.smeval_C_mul, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.RingTheory.Binomial
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 ℕ n) x * x + n • smeval (ascPochhammer ℕ n) x =
    smeval (ascPochhammer ℕ n) x * x + HSMul.hSMul (α := ℕ) (↑n : ℕ) (smeval (ascPochhammer ℕ n) x)

Tactic:
simp only [nsmul_eq_mul, Nat.cast_id]

Premises used: Nat.cast_id, nsmul_eq_mul