have : i ∈ Finset.range (n + 1) := by
  rw [Finset.mem_range] at *
  exact Nat.lt_add_right 1 hi
case left
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
⊢ Odd (f i)
case left
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
this : i ∈ Finset.range (n + 1)
⊢ Odd (f i)