rw [h4, ih, mul_right_comm]
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
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
h4 :
  ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
⊢ (∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)) *
      ∏ 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
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
h3 :
  ∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n.succ + 1)).erase x, f j =
    ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1)
h4 :
  ∏ x ∈ Finset.range (n + 1), (∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) =
    (∏ x ∈ Finset.range (n + 1), ∏ j ∈ (Finset.range (n + 1)).erase x, f j) * f (n + 1) ^ (n + 1)
⊢ ((∏ i ∈ Finset.range (n + 1), f i ^ ↑n) * ∏ j ∈ Finset.range (n + 1), f j) * f (n + 1) ^ (n + 1) =
    ((∏ x ∈ Finset.range (n + 1), f x ^ ↑n) * ∏ x ∈ Finset.range (n + 1), f x) * f (n + 1) ^ ↑n.succ