case zero
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
⊢ map f (pochhammer S Nat.zero) = pochhammer T Nat.zero

case succ
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
ih : map f (pochhammer S n) = pochhammer T n
⊢ map f (pochhammer S (Nat.succ n)) = pochhammer T (Nat.succ n)
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
⊢ map f (pochhammer S n) = pochhammer T n
induction' n with n ih
no goals
case zero
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
⊢ map f (pochhammer S Nat.zero) = pochhammer T Nat.zero
simp
no goals
case succ
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
ih : map f (pochhammer S n) = pochhammer T n
⊢ map f (pochhammer S (Nat.succ n)) = pochhammer T (Nat.succ n)
simp [ih, pochhammer_succ_left, map_comp]