have h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ((Nat.succ n):ℝ) =
          ∏ i ∈ Finset.range (n + 1), (f i ^ (n:ℝ) * f i) := by
   congr; funext x
   norm_cast
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 =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * 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
h2 : ∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ = ∏ i ∈ Finset.range (n + 1), f i ^ ↑n * f i
⊢ ∏ i ∈ Finset.range (n + 1 + 1), ∏ j ∈ (Finset.range (n + 1 + 1)).erase i, f j =
    (∏ i ∈ Finset.range (n + 1), f i ^ ↑n.succ) * f (n + 1) ^ ↑n.succ