S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = pochhammer ℕ (n + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer S (n + 1)) (X + 1) = pochhammer S (n + 1) + (n + 1) • comp (pochhammer S n) (X + 1)
suffices (pochhammer ℕ (n + 1)).comp (X + 1) =
    pochhammer ℕ (n + 1) + (n + 1) * (pochhammer ℕ n).comp (X + 1)
  by simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = X * comp (pochhammer ℕ n) (X + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = pochhammer ℕ (n + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
nth_rw 2 [pochhammer_succ_left]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = X * comp (pochhammer ℕ n) (X + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = X * comp (pochhammer ℕ n) (X + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
simp only
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (↑n + X + 1) * comp (pochhammer ℕ n) (X + 1) = (X + (↑n + 1)) * comp (pochhammer ℕ n) (X + 1)
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = X * comp (pochhammer ℕ n) (X + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
rw [← add_mul, pochhammer_succ_right ℕ n, mul_comp, mul_comm, add_comp, X_comp, nat_cast_comp,
  add_comm, ← add_assoc]
no goals
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (↑n + X + 1) * comp (pochhammer ℕ n) (X + 1) = (X + (↑n + 1)) * comp (pochhammer ℕ n) (X + 1)
ring
no goals
S : Type u
inst✝ : Semiring S
n : ℕ
this : comp (pochhammer ℕ (n + 1)) (X + 1) = pochhammer ℕ (n + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
⊢ comp (pochhammer S (n + 1)) (X + 1) = pochhammer S (n + 1) + (n + 1) • comp (pochhammer S n) (X + 1)
simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this