ring
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)
h7' : n + 1 ∉ (Finset.range (n + 1)).erase x
h7 : (Finset.range (n.succ + 1)).erase x = insert (n + 1) ((Finset.range (n + 1)).erase x)
⊢ f (n + 1) * ∏ x ∈ (Finset.range (n + 1)).erase x, f x = (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
no goals