awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
hn : natDegree (descPochhammer R 0) = 0
this : (HSub.hSub (α := R[X]) X (↑0 : R[X])).natDegree = 1
⊢ Ne (α := R[X]) (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 + 1)) = n + 1
this : (HSub.hSub (α := R[X]) X (↑(n + 1) : R[X])).natDegree = 1
⊢ Ne (α := R[X]) (descPochhammer R (n + 1)) 0

Tactic:
ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _

Premises used: 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 + 1)) = n + 1
this : (HSub.hSub (α := R[X]) X (↑(n + 1) : R[X])).natDegree = 1
⊢ Ne (α := R[X]) (descPochhammer R (n + 1)) 0

Tactic:
refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _

Premises used: Polynomial.ne_zero_of_natDegree_gt
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
zero : natDegree (descPochhammer R 0) = 0
succ : ∀ (n : ℕ) (hn : natDegree (descPochhammer R n) = n), natDegree (descPochhammer R (n + 1)) = n + 1
⊢ natDegree (descPochhammer R n) = n

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)
    rw [descPochhammer_succ_right,
        natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]
    cases n
    · simp
    · refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _

Premises used: Polynomial.natDegree_mul, descPochhammer_succ_right, Polynomial.ne_zero_of_natDegree_gt
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Ring S
n : ℕ
k : S
rw : eval k (descPochhammer S n * HSub.hSub (α := S[X]) X (↑n : S[X])) = eval k (descPochhammer S n) * (k - (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X - HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (descPochhammer S n) X) -
      eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₃ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (descPochhammer S n) (↑n : S[X])) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₄ :
  eval k (descPochhammer S n) * k - eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (descPochhammer S n)) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₅ :
  eval k (descPochhammer S n) * k -
      eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (descPochhammer S n)) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₆ :
  eval k (descPochhammer S n) * k - (↑n : S) * eval k (descPochhammer S n) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₇ :
  eval k (descPochhammer S n) * k - eval k (descPochhammer S n) * (↑n : S) =
    eval k (descPochhammer S n) * (k - (↑n : S))
rw₈ rw₉ : eval k (descPochhammer S n) * (k - (↑n : S)) = eval k (descPochhammer S n) * (k - (↑n : S))
⊢ eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - (↑n : S))

Tactic:
rw [descPochhammer_succ_right, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm, ← C_eq_natCast,
    eval_C_mul, Nat.cast_comm, ← mul_sub]

Premises used: Nat.cast_comm, mul_sub, Polynomial.C_eq_natCast, descPochhammer_succ_right, Polynomial.eval_mul_X, Polynomial.eval_sub, Polynomial.eval_C_mul
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
this :
  comp (descPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X 1) =
    descPochhammer ℤ (n + 1) -
      HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1)
⊢ comp (descPochhammer R (n + 1)) (HSub.hSub (α := R[X]) X 1) =
    descPochhammer R (n + 1) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 • comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)

Tactic:
simpa [map_comp] using congr_arg (Polynomial.map (Int.castRingHom R)) this

Premises used: congr_arg, Int.castRingHom, Polynomial.map, Polynomial.map_comp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
suffices :
  comp (descPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X 1) =
    descPochhammer ℤ (n + 1) -
      HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1)
⊢ comp (descPochhammer R (n + 1)) (HSub.hSub (α := R[X]) X 1) =
    descPochhammer R (n + 1) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 • comp (descPochhammer R n) (HSub.hSub (α := R[X]) X 1)

Tactic:
suffices (descPochhammer ℤ (n + 1)).comp (X - 1) =
      descPochhammer ℤ (n + 1) - (n + 1) * (descPochhammer ℤ n).comp (X - 1)
    by simpa [map_comp] using congr_arg (Polynomial.map (Int.castRingHom R)) this
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
rw :
  (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1) =
    (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1) * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1)
⊢ comp (descPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X 1) =
    X * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1) -
      HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1)

Tactic:
rw [← sub_mul, descPochhammer_succ_right ℤ n, mul_comp, mul_comm, sub_comp, X_comp, natCast_comp]

Premises used: Polynomial.X_comp, descPochhammer_succ_right, Int, sub_mul, Polynomial.natCast_comp, mul_comm, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ (HSub.hSub (α := ℤ[X]) X 1 - (↑n : ℤ[X])) * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1) =
    (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1) * comp (descPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X 1)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
zero : 1 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
zero₁ : 1 = comp 1 (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
zero₂ zero₃ : Eq (α := ℤ[X]) 1 1
⊢ descPochhammer ℤ 0 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)

Tactic:
rw [descPochhammer_zero, ascPochhammer_zero, one_comp]

Premises used: ascPochhammer_zero, Polynomial.one_comp, descPochhammer_zero
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
n : ℕ
ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)
succ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 + 1)
succ₁ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (X - (HAdd.hAdd (α := ℤ[X]) (↑n : ℤ[X]) 1 - 1))
succ₂ : descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₃ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₄ :
  descPochhammer ℤ n * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₅ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (X * comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₆ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1) * X).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))
succ₇ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    (comp (ascPochhammer ℤ n) (HAdd.hAdd (α := ℤ[X]) X 1)).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₈ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n) ((HAdd.hAdd (α := ℤ[X]) X 1).comp (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₉ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n)
        (comp X (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])) + comp 1 (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₁₀ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + comp 1 (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]))) *
      HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
succ₁₁ succ₁₂ :
  comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) =
    comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1) * HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X])
⊢ descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)

Tactic:
rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]

Premises used: sub_add, Polynomial.comp_assoc, Nat.cast_succ, Polynomial.X_comp, descPochhammer_succ_right, Polynomial.add_comp, Polynomial.X_mul, Polynomial.one_comp, Polynomial.mul_X_comp, add_sub_cancel_right, ascPochhammer_succ_left
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
n : ℕ
zero : descPochhammer ℤ 0 = comp (ascPochhammer ℤ 0) (HSub.hSub (α := ℤ[X]) X (↑0 : ℤ[X]) + 1)
succ :
  ∀ (n : ℕ) (ih : descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)),
    descPochhammer ℤ (n + 1) = comp (ascPochhammer ℤ (n + 1)) (HSub.hSub (α := ℤ[X]) X (↑(n + 1) : ℤ[X]) + 1)
⊢ descPochhammer ℤ n = comp (ascPochhammer ℤ n) (HSub.hSub (α := ℤ[X]) X (↑n : ℤ[X]) + 1)

Tactic:
induction n with
  | zero => rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
      ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]

Premises used: sub_add, Polynomial.comp_assoc, Nat.cast_succ, Polynomial.X_comp, descPochhammer_succ_right, Polynomial.add_comp, ascPochhammer_zero, Polynomial.X_mul, Polynomial.one_comp, Polynomial.mul_X_comp, add_sub_cancel_right, ascPochhammer_succ_left, descPochhammer_zero
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
r : R
zero : eval r 1 = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
zero₁ : 1 = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
zero₂ : 1 = eval (r - (↑0 : R) + 1) 1
zero₃ zero₄ : Eq.{u + 1} (α := R) 1 1
⊢ eval r (descPochhammer R 0) = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)

Tactic:
rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]

Premises used: ascPochhammer_zero, Polynomial.eval_one, descPochhammer_zero
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
⊢ HAdd.hAdd (α := R[X]) X 1 = map (algebraMap ℕ R) (HAdd.hAdd (α := ℕ[X]) X 1)

Tactic:
simp only [Polynomial.map_add, map_X,
      Polynomial.map_one]

Premises used: Polynomial.map_one, Polynomial.map_add, Polynomial.map_X
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)
succ : eval r (descPochhammer R (n + 1)) = eval (r - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (ascPochhammer R (n + 1))
succ₁ : eval r (descPochhammer R (n + 1)) = eval (r - (HAdd.hAdd (α := R) (↑n : R) 1 - 1)) (ascPochhammer R (n + 1))
succ₂ : eval r (descPochhammer R (n + 1)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₃ : eval r (descPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₄ : eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) = eval (r - (↑n : R)) (ascPochhammer R (n + 1))
succ₅ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (X * comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1))
succ₆ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1) * X)
succ₇ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (HAdd.hAdd (α := R[X]) X 1)) * (r - (↑n : R))
succ₈ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R)) (comp (ascPochhammer R n) (map (algebraMap ℕ R) (HAdd.hAdd (α := ℕ[X]) X 1))) * (r - (↑n : R))
succ₉ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (eval₂ (algebraMap ℕ R) (r - (↑n : R)) (HAdd.hAdd (α := ℕ[X]) X 1)) (ascPochhammer R n) * (r - (↑n : R))
succ₁₀ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (eval₂ (algebraMap ℕ R) (r - (↑n : R)) X + eval₂ (algebraMap ℕ R) (r - (↑n : R)) 1) (ascPochhammer R n) *
      (r - (↑n : R))
succ₁₁ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R) + eval₂ (algebraMap ℕ R) (r - (↑n : R)) 1) (ascPochhammer R n) * (r - (↑n : R))
succ₁₂ succ₁₃ :
  eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R)) =
    eval (r - (↑n : R) + 1) (ascPochhammer R n) * (r - (↑n : R))
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))

Tactic:
rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]

Premises used: sub_add, Nat.cast_succ, Polynomial.eval₂_one, Polynomial.X_mul, ascPochhammer_eval_comp, Polynomial.eval₂_X, descPochhammer_succ_eval, Polynomial.eval_mul_X, add_sub_cancel_right, ascPochhammer_succ_left, Polynomial.eval₂_add
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
r : R
n : ℕ
zero : eval r (descPochhammer R 0) = eval (r - (↑0 : R) + 1) (ascPochhammer R 0)
succ :
  ∀ (n : ℕ) (ih : eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)),
    eval r (descPochhammer R (n + 1)) = eval (r - (↑(n + 1) : R) + 1) (ascPochhammer R (n + 1))
⊢ eval r (descPochhammer R n) = eval (r - (↑n : R) + 1) (ascPochhammer R n)

Tactic:
induction n with
  | zero => rw [descPochhammer_zero, eval_one, ascPochhammer_zero, eval_one]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_eval, ih,
      ascPochhammer_succ_left, X_mul, eval_mul_X, show (X + 1 : R[X]) =
      (X + 1 : ℕ[X]).map (algebraMap ℕ R) by simp only [Polynomial.map_add, map_X,
      Polynomial.map_one], ascPochhammer_eval_comp, eval₂_add, eval₂_X, eval₂_one]

Premises used: sub_add, Nat.cast_succ, Polynomial.eval₂_one, ascPochhammer_zero, Polynomial.X_mul, ascPochhammer_eval_comp, Polynomial.eval₂_X, Polynomial.eval_one, descPochhammer_succ_eval, Polynomial.eval_mul_X, add_sub_cancel_right, ascPochhammer_succ_left, descPochhammer_zero, Polynomial.eval₂_add
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n : ℕ
⊢ descPochhammer R n * comp (descPochhammer R 0) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n m : ℕ
ih : descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)
succ :
  descPochhammer R n *
      (descPochhammer R m * HSub.hSub (α := R[X]) X (↑m : R[X])).comp (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))
succ₁ :
  descPochhammer R n *
      (comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
        (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))) =
    descPochhammer R (n + (m + 1))
succ₂ :
  descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) *
      (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + (m + 1))
succ₃ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + (m + 1))
succ₄ : descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) = descPochhammer R (n + m + 1)
succ₅ :
  descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + m) * HSub.hSub (α := R[X]) X (↑(n + m) : R[X])
succ₆ :
  descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + m) * (X - HAdd.hAdd (α := R[X]) (↑n : R[X]) (↑m : R[X]))
succ₇ succ₈ :
  descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X])) =
    descPochhammer R (n + m) * (HSub.hSub (α := R[X]) X (↑n : R[X]) - (↑m : R[X]))
⊢ descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
    descPochhammer R (n + (m + 1))

Tactic:
rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]

Premises used: add_assoc, mul_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub, Polynomial.mul_X_sub_intCast_comp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n m : ℕ
zero : descPochhammer R n * comp (descPochhammer R 0) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + 0)
succ :
  ∀ (m : ℕ)
    (ih :
      descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)),
    descPochhammer R n * comp (descPochhammer R (m + 1)) (HSub.hSub (α := R[X]) X (↑n : R[X])) =
      descPochhammer R (n + (m + 1))
⊢ descPochhammer R n * comp (descPochhammer R m) (HSub.hSub (α := R[X]) X (↑n : R[X])) = descPochhammer R (n + m)

Tactic:
induction m with
  | zero => simp
  | succ m ih =>
    rw [descPochhammer_succ_right, Polynomial.mul_X_sub_intCast_comp, ← mul_assoc, ih,
      ← add_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub]

Premises used: add_assoc, mul_assoc, descPochhammer_succ_right, Nat.cast_add, sub_add_eq_sub_sub, Polynomial.mul_X_sub_intCast_comp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
r : R
rw : eval (-r) 1 = HPow.hPow (α := R) (β := ℕ) (-1) 0 * eval r 1
⊢ eval (-r) (ascPochhammer R 0) = HPow.hPow (α := R) (β := ℕ) (-1) 0 * eval r (descPochhammer R 0)

Tactic:
rw [ascPochhammer_zero, descPochhammer_zero]

Premises used: ascPochhammer_zero, descPochhammer_zero
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
r : R
⊢ eval (-r) 1 = HPow.hPow (α := R) (β := ℕ) (-1) 0 * eval r 1

Tactic:
simp only [eval_one, pow_zero, mul_one]

Premises used: pow_zero, Polynomial.eval_one, mul_one
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
a b : ℕ
rw : eval (↑(a + b) : ℤ) (descPochhammer ℤ b) = (↑((a + 1).ascFactorial b) : ℤ)
rw₁ : Eq (α := ℤ) (↑((a + b).descFactorial b) : ℤ) (↑((a + 1).ascFactorial b) : ℤ)
rw₂ rw₃ : Eq (α := ℤ) (↑((a + 1).ascFactorial b) : ℤ) (↑((a + 1).ascFactorial b) : ℤ)
⊢ eval (HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ)) (descPochhammer ℤ b) = (↑((a + 1).ascFactorial b) : ℤ)

Tactic:
rw [← Nat.cast_add, descPochhammer_eval_eq_descFactorial ℤ (a + b) b,
    Nat.add_descFactorial_eq_ascFactorial]

Premises used: Int, Nat.cast_add, descPochhammer_eval_eq_descFactorial, HAdd.hAdd, Nat.add_descFactorial_eq_ascFactorial
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
k : ℕ
h : k < 0
⊢ eval (-(↑k : R)) (ascPochhammer R 0) = 0

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
k n : ℕ
ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0
h : k < n + 1
succ : eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
⊢ eval (-(↑k : R)) (ascPochhammer R (n + 1)) = 0

Tactic:
rw [ascPochhammer_succ_eval]

Premises used: ascPochhammer_succ_eval
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
k n : ℕ
ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0
h : k < n + 1
succ : ∀ (hkn : k < n), eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
succ₁ :
  ∀ (ih : ∀ (h : k < k), eval (-(↑k : R)) (ascPochhammer R k) = 0) (h : k < k + 1),
    eval (-(↑k : R)) (ascPochhammer R k) * HAdd.hAdd (α := R) (-(↑k : R)) (↑k : R) = 0
succ₂ : ∀ (hkn : n < k), eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0
⊢ eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0

Tactic:
rcases lt_trichotomy k n with hkn | rfl | hkn

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
k n : ℕ
ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0
h : k < n + 1
hkn : k < n
⊢ eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0

Tactic:
simp [ih hkn]
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
k : ℕ
ih : ∀ (h : k < k), eval (-(↑k : R)) (ascPochhammer R k) = 0
h : k < k + 1
⊢ eval (-(↑k : R)) (ascPochhammer R k) * HAdd.hAdd (α := R) (-(↑k : R)) (↑k : R) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
k n : ℕ
ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0
h : k < n + 1
hkn : n < k
⊢ eval (-(↑k : R)) (ascPochhammer R n) * HAdd.hAdd (α := R) (-(↑k : R)) (↑n : R) = 0

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
n k : ℕ
h : k < n
zero : ∀ (h : k < 0), eval (-(↑k : R)) (ascPochhammer R 0) = 0
succ :
  ∀ (n : ℕ) (ih : ∀ (h : k < n), eval (-(↑k : R)) (ascPochhammer R n) = 0) (h : k < n + 1),
    eval (-(↑k : R)) (ascPochhammer R (n + 1)) = 0
⊢ eval (-(↑k : R)) (ascPochhammer R n) = 0

Tactic:
induction n with
  | zero => contradiction
  | succ n ih =>
    rw [ascPochhammer_succ_eval]
    rcases lt_trichotomy k n with hkn | rfl | hkn
    · simp [ih hkn]
    · simp
    · lia

Premises used: ascPochhammer_succ_eval, rfl, lt_trichotomy
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
⊢ eval r (ascPochhammer R n) = 0 ↔ ∃ k < n, (↑k : R) = -r

Tactic:
⟨fun zero' ↦ ?_, fun hrn ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
n : ℕ
r : R
refine_1 : ∀ (zero' : eval r (ascPochhammer R n) = 0), ∃ k < n, (↑k : R) = -r
refine_2 : ∀ (hrn : ∃ k < n, (↑k : R) = -r), eval r (ascPochhammer R n) = 0
⊢ eval r (ascPochhammer R n) = 0 ↔ ∃ k < n, (↑k : R) = -r

Tactic:
refine ⟨fun zero' ↦ ?_, fun hrn ↦ ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
r : R
zero' : eval r (ascPochhammer R 0) = 0
⊢ ∃ k < 0, (↑k : R) = -r

Tactic:
simp only [ascPochhammer_zero, Polynomial.eval_one, one_ne_zero] at zero'

Premises used: ascPochhammer_zero, Polynomial.eval_one, one_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
R : Type u
inst : Ring R
inst_1 : IsDomain R
r : R
n : ℕ
ih : ∀ (zero' : eval r (ascPochhammer R n) = 0), ∃ k < n, (↑k : R) = -r
zero' : eval r (ascPochhammer R (n + 1)) = 0
⊢ eval r (ascPochhammer R n) = 0 ∨ r + (↑n : R) = 0

Tactic:
rw [ascPochhammer_succ_eval, mul_eq_zero] at zero'

Premises used: ascPochhammer_succ_eval, mul_eq_zero