Theorem: Imo1979P1.lemma9 (Compfiles/Imo1979P1.lean)

State before:
⊢ (∑ i ∈ Finset.range 330, 1 / ((660 + ↑i) * (1319 - ↑i))) * ↑(∏ j ∈ Finset.range 330, (660 + j) * (1319 - j)) =
    ↑(∑ i ∈ Finset.range 330, ∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))
Tactic:
simp_rw [Finset.sum_mul, div_mul_eq_mul_div, one_mul]
State after:
⊢ ∑ x ∈ Finset.range 330, ↑(∏ j ∈ Finset.range 330, (660 + j) * (1319 - j)) / ((660 + ↑x) * (1319 - ↑x)) =
    ↑(∑ i ∈ Finset.range 330, ∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))

State before:
⊢ ∑ x ∈ Finset.range 330, ↑(∏ j ∈ Finset.range 330, (660 + j) * (1319 - j)) / ((660 + ↑x) * (1319 - ↑x)) =
    ↑(∑ i ∈ Finset.range 330, ∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))
Tactic:
rw [Finset.sum_congr rfl lemma9']
State after:
⊢ ∑ x ∈ Finset.range 330, ↑(∏ j ∈ (Finset.range 330).erase x, (660 + j) * (1319 - j)) =
    ↑(∑ i ∈ Finset.range 330, ∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))

State before:
⊢ ∑ x ∈ Finset.range 330, ↑(∏ j ∈ (Finset.range 330).erase x, (660 + j) * (1319 - j)) =
    ↑(∑ i ∈ Finset.range 330, ∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))
Tactic:
push_cast
State after:
⊢ ∑ x ∈ Finset.range 330, ∏ x ∈ (Finset.range 330).erase x, (660 + ↑x) * ↑(1319 - x) =
    ∑ x ∈ Finset.range 330, ∏ x ∈ (Finset.range 330).erase x, (660 + ↑x) * ↑(1319 - x)

State before:
⊢ ∑ x ∈ Finset.range 330, ∏ x ∈ (Finset.range 330).erase x, (660 + ↑x) * ↑(1319 - x) =
    ∑ x ∈ Finset.range 330, ∏ x ∈ (Finset.range 330).erase x, (660 + ↑x) * ↑(1319 - x)
Tactic:
rfl
State after:
no goals