have h2 : ((660 + (i:ℚ)) * (1319 - (i:ℚ))) /
            ((660 + (i:ℚ)) * (1319 - (i:ℚ))) = 1 := by
  have h3 : (660 + (i:ℚ)) * (1319 - (i:ℚ)) ≠ 0 := by
    have h5 : (i: ℚ) < 330 := by norm_cast
    nlinarith
  exact div_self h3
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
⊢ (∏ x ∈ (Finset.range 330).erase i, (660 + ↑x) * ↑(1319 - x)) *
      ((660 + ↑i) * (1319 - ↑i) / ((660 + ↑i) * (1319 - ↑i))) =
    ∏ x ∈ (Finset.range 330).erase i, (660 + ↑x) * ↑(1319 - x)
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
h2 : (660 + ↑i) * (1319 - ↑i) / ((660 + ↑i) * (1319 - ↑i)) = 1
⊢ (∏ x ∈ (Finset.range 330).erase i, (660 + ↑x) * ↑(1319 - x)) *
      ((660 + ↑i) * (1319 - ↑i) / ((660 + ↑i) * (1319 - ↑i))) =
    ∏ x ∈ (Finset.range 330).erase i, (660 + ↑x) * ↑(1319 - x)