induction n
n : ℕ
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
case zero
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range 0, Odd (f i)) → Odd (∏ i ∈ Finset.range 0, f i)

case succ
f : ℕ → ℕ
n✝ : ℕ
a✝ : (∀ i ∈ Finset.range n✝, Odd (f i)) → Odd (∏ i ∈ Finset.range n✝, f i)
⊢ (∀ i ∈ Finset.range (n✝ + 1), Odd (f i)) → Odd (∏ i ∈ Finset.range (n✝ + 1), f i)