case zero
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer S n * comp (pochhammer S Nat.zero) (X + ↑n) = pochhammer S (n + Nat.zero)

case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : pochhammer S n * comp (pochhammer S m) (X + ↑n) = pochhammer S (n + m)
⊢ pochhammer S n * comp (pochhammer S (Nat.succ m)) (X + ↑n) = pochhammer S (n + Nat.succ m)
S : Type u
inst✝ : Semiring S
n m : ℕ
⊢ pochhammer S n * comp (pochhammer S m) (X + ↑n) = pochhammer S (n + m)
induction' m with m ih
no goals
case zero
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer S n * comp (pochhammer S Nat.zero) (X + ↑n) = pochhammer S (n + Nat.zero)
simp
no goals
case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : pochhammer S n * comp (pochhammer S m) (X + ↑n) = pochhammer S (n + m)
⊢ pochhammer S n * comp (pochhammer S (Nat.succ m)) (X + ↑n) = pochhammer S (n + Nat.succ m)
rw [pochhammer_succ_right, Polynomial.mul_X_add_nat_cast_comp, ← mul_assoc, ih,
  Nat.succ_eq_add_one, ← add_assoc, pochhammer_succ_right, Nat.cast_add, add_assoc]