awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
T : Type v
inst_1 : Semiring T
f : S →+* T
⊢ map f (ascPochhammer S 0) = ascPochhammer T 0

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

Tactic:
simp [ih, ascPochhammer_succ_left, map_comp]

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

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

Premises used: Polynomial.map_comp, ascPochhammer_succ_left
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
T : Type v
inst_1 : Semiring T
f : S →+* T
n : ℕ
t : T
rw : eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)
⊢ eval t (ascPochhammer T n) = eval₂ f t (ascPochhammer S n)

Tactic:
rw [← ascPochhammer_map f]

Premises used: ascPochhammer_map
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
T : Type v
inst_1 : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)

Tactic:
eval_map f t

Premises used: Polynomial.eval_map
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
T : Type v
inst_1 : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)

Tactic:
exact eval_map f t

Premises used: Polynomial.eval_map
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
R : Type u_1
inst_1 : CommSemiring R
n : ℕ
p : R[X]
inst_2 : Algebra R S
x : S
rw :
  eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x p) (ascPochhammer R n)
rw₁ : eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
rw₂ :
  eval x (comp (map (algebraMap R S) (ascPochhammer R n)) (map (algebraMap R S) p)) =
    eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
rw₃ : eval x (map (algebraMap R S) (comp (ascPochhammer R n) p)) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
rw₄ rw₅ : eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p) = eval₂ (algebraMap R S) x (comp (ascPochhammer R n) p)
⊢ eval x (comp (ascPochhammer S n) (map (algebraMap R S) p)) = eval (eval₂ (algebraMap R S) x p) (ascPochhammer S n)

Tactic:
rw [ascPochhammer_eval₂ (algebraMap R S), ← eval₂_comp', ← ascPochhammer_map (algebraMap R S),
    ← map_comp, eval_map]

Premises used: Polynomial.eval_map, Algebra.algebraMap, ascPochhammer_map, Polynomial.map_comp, ascPochhammer_eval₂, Polynomial.eval₂_comp'
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n k : ℕ
rw : (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (map (algebraMap ℕ S) (ascPochhammer ℕ n))
rw₁ : (↑(eval k (ascPochhammer ℕ n)) : S) = eval₂ (algebraMap ℕ S) (↑k : S) (ascPochhammer ℕ n)
rw₂ : (algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) = eval₂ (algebraMap ℕ S) (↑k : S) (ascPochhammer ℕ n)
rw₃ :
  Eq (α := S) ((algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) : S)
    ((algebraMap ℕ S : (a : ℕ) → S) (eval (↑k : ℕ) (ascPochhammer ℕ n)) : S)
rw₄ rw₅ :
  Eq (α := S) ((algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) : S)
    ((algebraMap ℕ S : (a : ℕ) → S) (eval k (ascPochhammer ℕ n)) : S)
⊢ (↑(eval k (ascPochhammer ℕ n)) : S) = eval (↑k : S) (ascPochhammer S n)

Tactic:
rw [← ascPochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S),
      eval₂_at_natCast, Nat.cast_id]

Premises used: Polynomial.eval_map, Nat.cast_id, Algebra.algebraMap, Polynomial.eval₂_at_natCast, ascPochhammer_map, Nat, eq_natCast
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
zero : eval 0 (ascPochhammer S 0) = if Eq (α := ℕ) 0 0 then 1 else 0
succ : ∀ (n : ℕ), eval 0 (ascPochhammer S (n + 1)) = if n + 1 = 0 then 1 else 0
⊢ eval 0 (ascPochhammer S n) = if n = 0 then 1 else 0

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

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

Tactic:
simp [X_mul, ascPochhammer_succ_left]

Premises used: Polynomial.X_mul, ascPochhammer_succ_left
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
⊢ eval 0 (ascPochhammer S 0) = 1

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

Tactic:
simp [ascPochhammer_eval_zero, h]

Premises used: ascPochhammer_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
h : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
⊢ Eq (α := S[X]) (map (algebraMap ℕ S) (ascPochhammer ℕ (n + 1)))
    (map (algebraMap ℕ S) (ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])))

Tactic:
apply_fun Polynomial.map (algebraMap ℕ S) at h

Premises used: Algebra.algebraMap, Nat, Polynomial.map
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
h :
  Eq (α := S[X]) (map (algebraMap ℕ S) (ascPochhammer ℕ (n + 1)))
    (map (algebraMap ℕ S) (ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])))
⊢ ascPochhammer S (n + 1) = ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])

Tactic:
simpa only [ascPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_natCast] using h

Premises used: Polynomial.map_mul, Polynomial.map_add, Polynomial.map_X, ascPochhammer_map, Polynomial.map_natCast
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
suffices : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
⊢ ascPochhammer S (n + 1) = ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])

Tactic:
suffices h : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + (n : ℕ[X])) by
    apply_fun Polynomial.map (algebraMap ℕ S) at h
    simpa only [ascPochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
      Polynomial.map_natCast] using h
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
⊢ ascPochhammer ℕ (HAdd.hAdd (α := ℕ) 0 1) = ascPochhammer ℕ 0 * HAdd.hAdd (α := ℕ[X]) X (↑0 : ℕ[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
rw : ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑n.succ : ℕ[X])
| ascPochhammer ℕ (n + 1 + 1)

Tactic:
rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]

Premises used: Nat.cast_succ, Polynomial.X_comp, add_assoc, mul_assoc, add_comm, Polynomial.add_comp, Polynomial.natCast_comp, Polynomial.mul_comp, OfNat.ofNat, ascPochhammer_succ_left
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])
conv_lhs : ascPochhammer ℕ (n + 1 + 1) = ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])
succ :
  ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑n.succ : ℕ[X]) =
    ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])
⊢ ascPochhammer ℕ (n + 1 + 1) = ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])

Tactic:
conv_lhs =>
      rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]

Premises used: Nat.cast_succ, Polynomial.X_comp, add_assoc, mul_assoc, add_comm, Polynomial.add_comp, Polynomial.natCast_comp, Polynomial.mul_comp, OfNat.ofNat, ascPochhammer_succ_left
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
zero : ascPochhammer ℕ (HAdd.hAdd (α := ℕ) 0 1) = ascPochhammer ℕ 0 * HAdd.hAdd (α := ℕ[X]) X (↑0 : ℕ[X])
succ :
  ∀ (n : ℕ) (ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])),
    ascPochhammer ℕ (n + 1 + 1) = ascPochhammer ℕ (n + 1) * HAdd.hAdd (α := ℕ[X]) X (↑(n + 1) : ℕ[X])
⊢ ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    conv_lhs =>
      rw [ascPochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← ascPochhammer_succ_left, add_comp,
          X_comp, natCast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]

Premises used: Nat.cast_succ, Polynomial.X_comp, add_assoc, mul_assoc, add_comm, Polynomial.add_comp, Polynomial.natCast_comp, Polynomial.mul_comp, OfNat.ofNat, ascPochhammer_succ_left
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
n : ℕ
k : S
rw : eval k (ascPochhammer S n * HAdd.hAdd (α := S[X]) X (↑n : S[X])) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₁ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X + HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₂ :
  eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) X) +
      eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₃ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (ascPochhammer S n) (↑n : S[X])) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₄ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) (↑n : S[X]) (ascPochhammer S n)) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₅ :
  eval k (ascPochhammer S n) * k + eval k (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (↑n : S)) (ascPochhammer S n)) =
    eval k (ascPochhammer S n) * (k + (↑n : S))
rw₆ :
  eval k (ascPochhammer S n) * k + (↑n : S) * eval k (ascPochhammer S n) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₇ :
  eval k (ascPochhammer S n) * k + eval k (ascPochhammer S n) * (↑n : S) = eval k (ascPochhammer S n) * (k + (↑n : S))
rw₈ rw₉ : eval k (ascPochhammer S n) * (k + (↑n : S)) = eval k (ascPochhammer S n) * (k + (↑n : S))
⊢ eval k (ascPochhammer S (n + 1)) = eval k (ascPochhammer S n) * (k + (↑n : S))

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

Premises used: Nat.cast_comm, Polynomial.C_eq_natCast, Polynomial.eval_add, mul_add, Polynomial.eval_mul_X, Polynomial.eval_C_mul, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
this :
  comp (ascPochhammer ℕ (n + 1)) (HAdd.hAdd (α := ℕ[X]) X 1) =
    ascPochhammer ℕ (n + 1) + HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) 1 * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)
⊢ comp (ascPochhammer S (n + 1)) (HAdd.hAdd (α := S[X]) X 1) =
    ascPochhammer S (n + 1) + (n + 1) • comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)

Tactic:
simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this

Premises used: congr_arg, Nat.castRingHom, Polynomial.map, Polynomial.map_comp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
suffices :
  comp (ascPochhammer ℕ (n + 1)) (HAdd.hAdd (α := ℕ[X]) X 1) =
    ascPochhammer ℕ (n + 1) + HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) 1 * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)
⊢ comp (ascPochhammer S (n + 1)) (HAdd.hAdd (α := S[X]) X 1) =
    ascPochhammer S (n + 1) + (n + 1) • comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)

Tactic:
suffices (ascPochhammer ℕ (n + 1)).comp (X + 1) =
      ascPochhammer ℕ (n + 1) + (n + 1) * (ascPochhammer ℕ n).comp (X + 1)
    by simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
rw :
  (HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) X + 1) * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1) =
    (X + HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) 1) * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)
⊢ comp (ascPochhammer ℕ (n + 1)) (HAdd.hAdd (α := ℕ[X]) X 1) =
    X * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1) +
      HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) 1 * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)

Tactic:
rw [← add_mul, ascPochhammer_succ_right ℕ n, mul_comp, mul_comm, add_comp, X_comp, natCast_comp,
    add_comm, ← add_assoc]

Premises used: add_mul, Polynomial.X_comp, add_assoc, add_comm, Polynomial.add_comp, Nat, Polynomial.natCast_comp, mul_comm, Polynomial.mul_comp, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
⊢ (HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) X + 1) * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1) =
    (X + HAdd.hAdd (α := ℕ[X]) (↑n : ℕ[X]) 1) * comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
⊢ ascPochhammer S n * comp (ascPochhammer S 0) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + 0)

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

Tactic:
rw [ascPochhammer_succ_right, Polynomial.mul_X_add_natCast_comp, ← mul_assoc, ih,
      ← add_assoc, ascPochhammer_succ_right, Nat.cast_add, add_assoc]

Premises used: add_assoc, mul_assoc, Nat.cast_add, Polynomial.mul_X_add_natCast_comp, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n m : ℕ
zero : ascPochhammer S n * comp (ascPochhammer S 0) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + 0)
succ :
  ∀ (m : ℕ)
    (ih : ascPochhammer S n * comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + m)),
    ascPochhammer S n * comp (ascPochhammer S (m + 1)) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) =
      ascPochhammer S (n + (m + 1))
⊢ ascPochhammer S n * comp (ascPochhammer S m) (HAdd.hAdd (α := S[X]) X (↑n : S[X])) = ascPochhammer S (n + m)

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

Premises used: add_assoc, mul_assoc, Nat.cast_add, Polynomial.mul_X_add_natCast_comp, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
n : ℕ
rw : eval n 1 = n.ascFactorial 0
rw₁ : 1 = n.ascFactorial 0
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ eval n (ascPochhammer ℕ 0) = n.ascFactorial 0

Tactic:
rw [ascPochhammer_zero, eval_one, Nat.ascFactorial_zero]

Premises used: Nat.ascFactorial_zero, ascPochhammer_zero, Polynomial.eval_one
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
n t : ℕ
rw : eval n (ascPochhammer ℕ t * HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₁ : eval n (ascPochhammer ℕ t) * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₂ : n.ascFactorial t * eval n (HAdd.hAdd (α := ℕ[X]) X (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₃ : n.ascFactorial t * (eval n X + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₄ : n.ascFactorial t * (n + eval n (↑t : ℕ[X])) = n.ascFactorial (t + 1)
rw₅ : n.ascFactorial t * (n + (↑t : ℕ)) = n.ascFactorial (t + 1)
rw₆ : n.ascFactorial t * (n + t) = n.ascFactorial (t + 1)
rw₇ : n.ascFactorial t * (n + t) = (n + t) * n.ascFactorial t
rw₈ rw₉ : (n + t) * n.ascFactorial t = (n + t) * n.ascFactorial t
⊢ eval n (ascPochhammer ℕ (t + 1)) = n.ascFactorial (t + 1)

Tactic:
rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
      eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]

Premises used: Nat.cast_id, Polynomial.eval_X, Polynomial.eval_natCast, Nat.ascFactorial_succ, Polynomial.eval_mul, Polynomial.eval_add, mul_comm, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
n k : ℕ
norm_cast : Eq.{u_1 + 1} (α := S) (↑(eval n (ascPochhammer ℕ k)) : S) (↑(n.ascFactorial k) : S)
⊢ eval (↑n : S) (ascPochhammer S k) = (↑(n.ascFactorial k) : S)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u_1
inst : Semiring S
n k : ℕ
rw rw₁ : Eq.{u_1 + 1} (α := S) (↑(n.ascFactorial k) : S) (↑(n.ascFactorial k) : S)
⊢ Eq.{u_1 + 1} (α := S) (↑(eval n (ascPochhammer ℕ k)) : S) (↑(n.ascFactorial k) : S)

Tactic:
rw [ascPochhammer_nat_eq_ascFactorial]

Premises used: ascPochhammer_nat_eq_ascFactorial
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
a b : ℕ
rw : a.ascFactorial b = (a + b - 1).descFactorial b
rw₁ rw₂ : a.ascFactorial b = a.ascFactorial b
⊢ eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b

Tactic:
rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']

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

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

Tactic:
rw [ascPochhammer_nat_eq_descFactorial]

Premises used: ascPochhammer_nat_eq_descFactorial
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
⊢ natDegree (ascPochhammer S 0) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
n : ℕ
hn : natDegree (ascPochhammer S n) = n
⊢ (HAdd.hAdd (α := S[X]) X (↑n : S[X])).natDegree = 1

Tactic:
have : natDegree (X + (n : S[X])) = 1 := natDegree_X_add_C (n : S)
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
n : ℕ
hn : natDegree (ascPochhammer S n) = n
this : (HAdd.hAdd (α := S[X]) X (↑n : S[X])).natDegree = 1
rw : Ne (α := S[X]) (ascPochhammer S n) 0
⊢ natDegree (ascPochhammer S (n + 1)) = n + 1

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

Premises used: Polynomial.natDegree_mul, Polynomial.ne_zero_of_natDegree_gt, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
n : ℕ
hn : natDegree (ascPochhammer S n) = n
this : (HAdd.hAdd (α := S[X]) X (↑n : S[X])).natDegree = 1
zero :
  ∀ (hn : natDegree (ascPochhammer S 0) = 0) (this : (HAdd.hAdd (α := S[X]) X (↑0 : S[X])).natDegree = 1),
    Ne (α := S[X]) (ascPochhammer S 0) 0
succ :
  ∀ (n : ℕ) (hn : natDegree (ascPochhammer S (n + 1)) = n + 1)
    (this : (HAdd.hAdd (α := S[X]) X (↑(n + 1) : S[X])).natDegree = 1), Ne (α := S[X]) (ascPochhammer S (n + 1)) 0
⊢ Ne (α := S[X]) (ascPochhammer S n) 0

Tactic:
cases n
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
hn : natDegree (ascPochhammer S 0) = 0
this : (HAdd.hAdd (α := S[X]) X (↑0 : S[X])).natDegree = 1
⊢ Ne (α := S[X]) (ascPochhammer S 0) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
n : ℕ
hn : natDegree (ascPochhammer S (n + 1)) = n + 1
this : (HAdd.hAdd (α := S[X]) X (↑(n + 1) : S[X])).natDegree = 1
⊢ Ne (α := S[X]) (ascPochhammer S (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:
S : Type u
inst : Semiring S
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
n : ℕ
hn : natDegree (ascPochhammer S (n + 1)) = n + 1
this : (HAdd.hAdd (α := S[X]) X (↑(n + 1) : S[X])).natDegree = 1
⊢ Ne (α := S[X]) (ascPochhammer S (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:
S : Type u
inst : Semiring S
n : ℕ
inst_1 : NoZeroDivisors S
inst_2 : Nontrivial S
zero : natDegree (ascPochhammer S 0) = 0
succ : ∀ (n : ℕ) (hn : natDegree (ascPochhammer S n) = n), natDegree (ascPochhammer S (n + 1)) = n + 1
⊢ natDegree (ascPochhammer S n) = n

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    have : natDegree (X + (n : S[X])) = 1 := natDegree_X_add_C (n : S)
    rw [ascPochhammer_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, Polynomial.ne_zero_of_natDegree_gt, 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
zero : LT.lt.{u_1} (α := S) 0 1
⊢ 0 < eval s (ascPochhammer S 0)

Tactic:
simp only [ascPochhammer_zero, eval_one]

Premises used: ascPochhammer_zero, Polynomial.eval_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
⊢ LT.lt.{u_1} (α := S) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one