rw [Finset.prod_range_succ, lemma2']
case 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 + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ
case 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
⊢ (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase x, f j) * ∏ j ∈ Finset.range (n + 1), f j =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ