rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_range]
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)
⊢ ∏ 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)
no goals