rw [Finset.prod_range_succ]
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
⊢ ∏ i ∈ Finset.range (n.succ + 1), f i ^ ↑n.succ = (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ
no goals