rw [Finset.mem_range] at *
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)
i : ℕ
hi : i ∈ Finset.range n
⊢ i ∈ Finset.range (n + 1)
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)
i : ℕ
hi : i < n
⊢ i < n + 1