rw [Finset.prod_range_succ, Nat.odd_mul]
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ i ∈ Finset.range (n + 1), f i)
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x) ∧ Odd (f n)