simp_all
f : ℕ → ℝ
n : ℕ
ih : ∏ i ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase i, f j = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ n + 1 ∉ (Finset.range (n + 1)).erase x
no goals