awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
h : 0 < s
⊢ LT.lt.{u_1} (α := S) 0 1

Tactic:
exact zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
succ : 0 < eval s (ascPochhammer S n) * (s + (↑n : S))
⊢ 0 < eval s (ascPochhammer S (n + 1))

Tactic:
rw [ascPochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_natCast_mul, eval_mul_X,
      Nat.cast_comm, ← mul_add]

Premises used: Nat.cast_comm, Polynomial.eval_natCast_mul, Polynomial.eval_add, mul_add, Polynomial.eval_mul_X, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n) * (s + (↑n : S))

Tactic:
mul_pos ih (lt_of_lt_of_le h (le_add_of_nonneg_right (Nat.cast_nonneg n)))

Premises used: Nat.cast_nonneg, mul_pos, le_add_of_nonneg_right, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n) * (s + (↑n : S))

Tactic:
exact mul_pos ih (lt_of_lt_of_le h (le_add_of_nonneg_right (Nat.cast_nonneg n)))

Premises used: Nat.cast_nonneg, mul_pos, le_add_of_nonneg_right, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
inst_1 : PartialOrder S
inst_2 : IsStrictOrderedRing S
n : ℕ
s : S
h : 0 < s
zero : 0 < eval s (ascPochhammer S 0)
succ : ∀ (n : ℕ) (ih : 0 < eval s (ascPochhammer S n)), 0 < eval s (ascPochhammer S (n + 1))
⊢ 0 < eval s (ascPochhammer S n)

Tactic:
induction n with
  | zero =>
    simp only [ascPochhammer_zero, eval_one]
    exact zero_lt_one
  | succ n ih =>
    rw [ascPochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_natCast_mul, eval_mul_X,
      Nat.cast_comm, ← mul_add]
    exact mul_pos ih (lt_of_lt_of_le h (le_add_of_nonneg_right (Nat.cast_nonneg n)))

Premises used: Nat.cast_comm, zero_lt_one, ascPochhammer_zero, Polynomial.eval_natCast_mul, Polynomial.eval_add, Polynomial.eval_one, mul_add, Polynomial.eval_mul_X, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_2
inst : Semiring S
n : ℕ
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  Eq.{u_2 + 1} (α := S) (↑(eval 1 (ascPochhammer ℕ n)) : S) (↑n ! : S)
rw_mod_cast₆ : Eq.{u_2 + 1} (α := S) (↑(ascFactorial 1 n) : S) (↑n ! : S)
⊢ eval 1 (ascPochhammer S n) = (↑n ! : S)

Tactic:
rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.one_ascFactorial]

Premises used: Nat.one_ascFactorial, ascPochhammer_nat_eq_ascFactorial
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_2
inst : Semiring S
r n : ℕ
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  Eq.{u_2 + 1} (α := S) (↑(r ! * eval (r + 1) (ascPochhammer ℕ n)) : S) (↑(r + n)! : S)
rw_mod_cast₆ : Eq.{u_2 + 1} (α := S) (↑(r ! * (r + 1).ascFactorial n) : S) (↑(r + n)! : S)
⊢ (↑r ! : S) * eval (HAdd.hAdd (α := S) (↑r : S) 1) (ascPochhammer S n) = (↑(r + n)! : S)

Tactic:
rw_mod_cast [ascPochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]

Premises used: Nat.factorial_mul_ascFactorial, ascPochhammer_nat_eq_ascFactorial
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
r : ℕ
pos : ∀ (h : r = 0), 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)
neg : ∀ (h : ¬r = 0), 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)
⊢ 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

Tactic:
by_cases h : r = 0
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
r : ℕ
h : r = 0
⊢ 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

Tactic:
simp only [h, zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, zero_add
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
r : ℕ
h : ¬r = 0
⊢ 0 * eval (HAdd.hAdd (α := ℕ) 0 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

Tactic:
simp only [ascPochhammer_eval_zero, zero_mul, if_neg h, mul_zero]

Premises used: MulZeroClass.zero_mul, ascPochhammer_eval_zero, MulZeroClass.mul_zero, if_neg
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
r k : ℕ
⊢ (k + 1) * eval (k + 1 + 1) (ascPochhammer ℕ r) = (k + 1 + r) * eval (k + 1) (ascPochhammer ℕ r)

Tactic:
simp only [ascPochhammer_nat_eq_ascFactorial, Nat.succ_ascFactorial, add_right_comm]

Premises used: add_right_comm, ascPochhammer_nat_eq_ascFactorial, Nat.succ_ascFactorial
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
r n : ℕ
⊢ (↑n : S) * eval (HAdd.hAdd (α := S) (↑n : S) 1) (ascPochhammer S r) =
    HAdd.hAdd (α := S) (↑n : S) (↑r : S) * eval (↑n : S) (ascPochhammer S r)

Tactic:
mod_cast congr_arg Nat.cast (ascPochhammer_nat_eval_succ r n)

Premises used: Nat.cast_mul._simp_1, Polynomial.eval, HMul.hMul, congrArg, Nat.cast_add._simp_1, ascPochhammer, cast, Nat.cast, congr_arg, ascPochhammer_nat_eval_succ, ascPochhammer_eval_cast._simp_1, HAdd.hAdd, Nat, congr, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
rw : (↑(eval a (ascPochhammer ℕ b)) : S) = eval (↑a : S) (ascPochhammer S b)
rw₁ rw₂ : eval (↑a : S) (ascPochhammer S b) = eval (↑a : S) (ascPochhammer S b)
⊢ (↑(a.ascFactorial b) : S) = eval (↑a : S) (ascPochhammer S b)

Tactic:
rw [← ascPochhammer_nat_eq_ascFactorial, ascPochhammer_eval_cast]

Premises used: ascPochhammer_eval_cast, ascPochhammer_nat_eq_ascFactorial
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
rw : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
⊢ (↑(a.descFactorial b) : S) = eval (↑(a - (b - 1)) : S) (ascPochhammer S b)

Tactic:
rw [← ascPochhammer_eval_cast, ascPochhammer_nat_eq_descFactorial]

Premises used: ascPochhammer_nat_eq_descFactorial, ascPochhammer_eval_cast
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial 0) : S) (↑((a - HSub.hSub (α := ℕ) 0 1 + 0 - 1).descFactorial 0) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
succ : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 1)) : S) (↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1)) : S)

Tactic:
simp_rw [add_succ, Nat.add_one_sub_one]

Premises used: Nat.add_one_sub_one, Nat.add_succ
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
succ :
  ∀ (h : a ≤ b),
    Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
succ₁ :
  ∀ (h : b ≤ a),
    Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)

Tactic:
obtain h | h := le_total a b

Premises used: le_total
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h_1 : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
h : a ≤ b
rw : a - b + b ≤ b
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)

Tactic:
rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]

Premises used: Nat.descFactorial_of_lt, Nat.lt_succ_of_le
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h_1 : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
h : a ≤ b
rw : 0 + b ≤ b
rw₁ rw₂ : b ≤ b
⊢ a - b + b ≤ b

Tactic:
rw [tsub_eq_zero_iff_le.mpr h, zero_add]

Premises used: Iff.mpr, tsub_eq_zero_iff_le, zero_add
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a b_1 b : ℕ
h_1 : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)
h : b ≤ a
succ succ₁ : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑(a.descFactorial (b + 0).succ) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 0).succ) : S) (↑((a - b + b).descFactorial (b + 0).succ) : S)

Tactic:
rw [tsub_add_cancel_of_le h]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a b : ℕ
zero : Eq.{u_1 + 1} (α := S) (↑(a.descFactorial 0) : S) (↑((a - HSub.hSub (α := ℕ) 0 1 + 0 - 1).descFactorial 0) : S)
succ :
  ∀ (b : ℕ),
    Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S) →
      Eq.{u_1 + 1} (α := S) (↑(a.descFactorial (b + 1)) : S)
        (↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1)) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(a.descFactorial b) : S) (↑((a - (b - 1) + b - 1).descFactorial b) : S)

Tactic:
induction b with
  | zero => simp
  | succ b =>
    simp_rw [add_succ, Nat.add_one_sub_one]
    obtain h | h := le_total a b
    · rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
      rw [tsub_eq_zero_iff_le.mpr h, zero_add]
    · rw [tsub_add_cancel_of_le h]

Premises used: Nat.add_one_sub_one, Nat.descFactorial_of_lt, Nat.lt_succ_of_le, le_total, zero_add, Nat.add_succ, Nat.zero, Nat.succ
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
a : ℕ
rw : (↑(ascFactorial 1 a) : S) = eval 1 (ascPochhammer S a)
rw₁ : eval (↑1 : S) (ascPochhammer S a) = eval 1 (ascPochhammer S a)
rw₂ rw₃ : eval 1 (ascPochhammer S a) = eval 1 (ascPochhammer S a)
⊢ (↑a ! : S) = eval 1 (ascPochhammer S a)

Tactic:
rw [← one_ascFactorial, cast_ascFactorial, cast_one]

Premises used: Nat.cast_ascFactorial, Nat.one_ascFactorial, Nat.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
⊢ Eq (α := R[X]) (descPochhammer R 0) 1

Tactic:
rfl

Premises used: descPochhammer, rfl
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
⊢ Eq (α := R[X]) (descPochhammer R 1) X

Tactic:
simp [descPochhammer]

Premises used: descPochhammer
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
rw rw₁ :
  X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1) = X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)
⊢ descPochhammer R (n + 1) = X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)

Tactic:
rw [descPochhammer]

Premises used: descPochhammer
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
⊢ Monic (descPochhammer R 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
⊢ (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1

Tactic:
have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
⊢ (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0

Tactic:
have : natDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R)
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
n : ℕ
hn : Monic (descPochhammer R n)
h : (HSub.hSub (α := R[X]) X 1).leadingCoeff = 1
this : (HSub.hSub (α := R[X]) X 1).natDegree ≠ 0
succ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).Monic
succ₁ : (X * comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (descPochhammer R n) * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) =
    1
succ₄ : leadingCoeff X * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
succ₅ : 1 * (1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n)) = 1
succ₆ : 1 * (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n) = 1
succ₇ : (HSub.hSub (α := R[X]) X 1).leadingCoeff ^ natDegree (descPochhammer R n) = 1
succ₈ : HPow.hPow (α := R) 1 (natDegree (descPochhammer R n)) = 1
succ₉ succ₁₀ : Eq.{u + 1} (α := R) 1 1
⊢ Monic (descPochhammer R (n + 1))

Tactic:
rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]

Premises used: one_pow, Polynomial.leadingCoeff_mul, descPochhammer_succ_left, Polynomial.leadingCoeff_comp, Polynomial.Monic.def, one_mul, Polynomial.monic_X
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
inst_1 : Nontrivial R
inst_2 : NoZeroDivisors R
zero : Monic (descPochhammer R 0)
succ : ∀ (n : ℕ) (hn : Monic (descPochhammer R n)), Monic (descPochhammer R (n + 1))
⊢ Monic (descPochhammer R n)

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1
    have : natDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R)
    rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]

Premises used: one_pow, Polynomial.leadingCoeff_mul, descPochhammer_succ_left, Polynomial.Monic.def, one_mul, Polynomial.monic_X
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
T : Type v
inst_1 : Ring T
f : R →+* T
⊢ map f (descPochhammer R 0) = descPochhammer T 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
T : Type v
inst_1 : Ring T
f : R →+* T
n : ℕ
ih : map f (descPochhammer R n) = descPochhammer T n
⊢ map f (descPochhammer R (n + 1)) = descPochhammer T (n + 1)

Tactic:
simp [ih, descPochhammer_succ_left, map_comp]

Premises used: descPochhammer_succ_left, Polynomial.map_comp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
T : Type v
inst_1 : Ring T
f : R →+* T
n : ℕ
zero : map f (descPochhammer R 0) = descPochhammer T 0
succ :
  ∀ (n : ℕ) (ih : map f (descPochhammer R n) = descPochhammer T n),
    map f (descPochhammer R (n + 1)) = descPochhammer T (n + 1)
⊢ map f (descPochhammer R n) = descPochhammer T n

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [ih, descPochhammer_succ_left, map_comp]

Premises used: descPochhammer_succ_left, Polynomial.map_comp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
k : ℤ
rw : (algebraMap ℤ R : (a : ℤ) → R) (eval k (descPochhammer ℤ n)) = eval₂ (algebraMap ℤ R) (↑k : R) (descPochhammer ℤ n)
⊢ (↑(eval k (descPochhammer ℤ n)) : R) = eval (↑k : R) (descPochhammer R n)

Tactic:
rw [← descPochhammer_map (algebraMap ℤ R), eval_map, ← eq_intCast (algebraMap ℤ R)]

Premises used: Polynomial.eval_map, Algebra.algebraMap, descPochhammer_map, Int, eq_intCast
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
k : ℤ
⊢ (algebraMap ℤ R : (a : ℤ) → R) (eval k (descPochhammer ℤ n)) = eval₂ (algebraMap ℤ R) (↑k : R) (descPochhammer ℤ n)

Tactic:
simp only [algebraMap_int_eq, eq_intCast, eval₂_at_intCast, Int.cast_id]

Premises used: eq_intCast, Polynomial.eval₂_at_intCast, Int.cast_id, algebraMap_int_eq
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
zero : eval 0 (descPochhammer R 0) = if Eq (α := ℕ) 0 0 then 1 else 0
succ : ∀ (n : ℕ), eval 0 (descPochhammer R (n + 1)) = if n + 1 = 0 then 1 else 0
⊢ eval 0 (descPochhammer R n) = if n = 0 then 1 else 0

Tactic:
cases n
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
⊢ eval 0 (descPochhammer R 0) = if Eq (α := ℕ) 0 0 then 1 else 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ eval 0 (descPochhammer R (n + 1)) = if n + 1 = 0 then 1 else 0

Tactic:
simp [X_mul, descPochhammer_succ_left]

Premises used: descPochhammer_succ_left, Polynomial.X_mul
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
⊢ eval 0 (descPochhammer R 0) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
h : n ≠ 0
⊢ eval 0 (descPochhammer R n) = 0

Tactic:
simp [descPochhammer_eval_zero, h]

Premises used: descPochhammer_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ Eq (α := R[X]) (map (algebraMap ℤ R) (descPochhammer ℤ (n + 1)))
    (map (algebraMap ℤ R) (descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])))

Tactic:
apply_fun Polynomial.map (algebraMap ℤ R) at h

Premises used: Algebra.algebraMap, Int, Polynomial.map
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
h :
  Eq (α := R[X]) (map (algebraMap ℤ R) (descPochhammer ℤ (n + 1)))
    (map (algebraMap ℤ R) (descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])))
⊢ descPochhammer R (n + 1) = descPochhammer R n * HSub.hSub (α := R[X]) X (↑n : R[X])

Tactic:
simpa [descPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_intCast] using h

Premises used: Polynomial.map_mul, Polynomial.map_add, descPochhammer_map, Polynomial.map_X, Polynomial.map_intCast
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
suffices : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ descPochhammer R (n + 1) = descPochhammer R n * HSub.hSub (α := R[X]) X (↑n : R[X])

Tactic:
suffices h : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * (X - (n : ℤ[X])) by
    apply_fun Polynomial.map (algebraMap ℤ R) at h
    simpa [descPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_intCast] using h
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
⊢ descPochhammer ℤ (HAdd.hAdd (α := ℕ) 0 1) = descPochhammer ℤ 0 * HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X])

Tactic:
simp [descPochhammer]

Premises used: descPochhammer
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
rw : descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X]))
| descPochhammer ℤ (n + 1 + 1)

Tactic:
rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]

Premises used: Polynomial.X_comp, mul_assoc, descPochhammer_succ_left, Polynomial.natCast_comp, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ :
  descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])
⊢ descPochhammer ℤ (n + 1 + 1) = descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])

Tactic:
conv_lhs =>
      rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]

Premises used: Polynomial.X_comp, mul_assoc, descPochhammer_succ_left, Polynomial.natCast_comp, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ :
  descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) (↑1 : ℤ[X]))
succ₁ :
  descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1)
succ₂ succ₃ :
  descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X]))
⊢ descPochhammer ℤ (n + 1) * (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) =
    descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])

Tactic:
rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]

Premises used: Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
zero : descPochhammer ℤ (HAdd.hAdd (α := ℕ) 0 1) = descPochhammer ℤ 0 * HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X])
succ :
  ∀ (n : ℕ) (ih : descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])),
    descPochhammer ℤ (n + 1 + 1) = descPochhammer ℤ (n + 1) * HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X])
⊢ descPochhammer ℤ (n + 1) = descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])

Tactic:
induction n with
  | zero => simp [descPochhammer]
  | succ n ih =>
    conv_lhs =>
      rw [descPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← descPochhammer_succ_left, sub_comp,
          X_comp, natCast_comp]
    rw [Nat.cast_add, Nat.cast_one, sub_add_eq_sub_sub_swap]

Premises used: descPochhammer, Polynomial.X_comp, mul_assoc, descPochhammer_succ_left, Nat.cast_add, Polynomial.natCast_comp, Polynomial.mul_comp, Nat.cast_one, Polynomial.sub_comp, sub_add_eq_sub_sub_swap
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
⊢ natDegree (descPochhammer R 0) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
n : ℕ
hn : natDegree (descPochhammer R n) = n
⊢ (HSub.hSub (α := R[X]) X (↑n : R[X])).natDegree = 1

Tactic:
have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
n : ℕ
hn : natDegree (descPochhammer R n) = n
this : (HSub.hSub (α := R[X]) X (↑n : R[X])).natDegree = 1
rw : Ne (α := R[X]) (descPochhammer R n) 0
⊢ natDegree (descPochhammer R (n + 1)) = n + 1

Tactic:
rw [descPochhammer_succ_right,
        natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]

Premises used: Polynomial.natDegree_mul, descPochhammer_succ_right, Polynomial.ne_zero_of_natDegree_gt
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
n : ℕ
hn : natDegree (descPochhammer R n) = n
this : (HSub.hSub (α := R[X]) X (↑n : R[X])).natDegree = 1
zero :
  ∀ (hn : natDegree (descPochhammer R 0) = 0) (this : (HSub.hSub (α := R[X]) X (↑0 : R[X])).natDegree = 1),
    Ne (α := R[X]) (descPochhammer R 0) 0
succ :
  ∀ (n : ℕ) (hn : natDegree (descPochhammer R (n + 1)) = n + 1)
    (this : (HSub.hSub (α := R[X]) X (↑(n + 1) : R[X])).natDegree = 1), Ne (α := R[X]) (descPochhammer R (n + 1)) 0
⊢ Ne (α := R[X]) (descPochhammer R n) 0

Tactic:
cases n