S : Type u
inst✝ : Semiring S
n : ℕ
h : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)

case h
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
suffices h : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + (n : ℕ[X]))
case h.zero
S : Type u
inst✝ : Semiring S
⊢ pochhammer ℕ (Nat.zero + 1) = pochhammer ℕ Nat.zero * (X + ↑Nat.zero)

case h.succ
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
⊢ pochhammer ℕ (Nat.succ n + 1) = pochhammer ℕ (Nat.succ n) * (X + ↑(Nat.succ n))
case h
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
induction' n with n ih
S : Type u
inst✝ : Semiring S
n : ℕ
h : map (algebraMap ℕ S) (pochhammer ℕ (n + 1)) = map (algebraMap ℕ S) (pochhammer ℕ n * (X + ↑n))
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
S : Type u
inst✝ : Semiring S
n : ℕ
h : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
apply_fun Polynomial.map (algebraMap ℕ S) at h
no goals
S : Type u
inst✝ : Semiring S
n : ℕ
h : map (algebraMap ℕ S) (pochhammer ℕ (n + 1)) = map (algebraMap ℕ S) (pochhammer ℕ n * (X + ↑n))
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
simpa only [pochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X,
  Polynomial.map_nat_cast] using h
no goals
case h.zero
S : Type u
inst✝ : Semiring S
⊢ pochhammer ℕ (Nat.zero + 1) = pochhammer ℕ Nat.zero * (X + ↑Nat.zero)
simp
no goals
case h.succ
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
⊢ pochhammer ℕ (Nat.succ n + 1) = pochhammer ℕ (Nat.succ n) * (X + ↑(Nat.succ n))
conv_lhs =>
  rw [pochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← pochhammer_succ_left, add_comp, X_comp,
    nat_cast_comp, add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]