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

State before:
i : ℕ
hi : i ∈ Finset.range 330
⊢ ↑(∏ j ∈ Finset.range 330, (660 + j) * (1319 - j)) / ((660 + ↑i) * (1319 - ↑i)) =
    ↑(∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))
Tactic:
rw [←Finset.prod_erase_mul _ _ hi]
State after:
i : ℕ
hi : i ∈ Finset.range 330
⊢ ↑((∏ x ∈ (Finset.range 330).erase i, (660 + x) * (1319 - x)) * ((660 + i) * (1319 - i))) /
      ((660 + ↑i) * (1319 - ↑i)) =
    ↑(∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))

State before:
i : ℕ
hi : i ∈ Finset.range 330
⊢ ↑((∏ x ∈ (Finset.range 330).erase i, (660 + x) * (1319 - x)) * ((660 + i) * (1319 - i))) /
      ((660 + ↑i) * (1319 - ↑i)) =
    ↑(∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))
Tactic:
rw [Finset.mem_range] at hi
State after:
i : ℕ
hi : i < 330
⊢ ↑((∏ x ∈ (Finset.range 330).erase i, (660 + x) * (1319 - x)) * ((660 + i) * (1319 - i))) /
      ((660 + ↑i) * (1319 - ↑i)) =
    ↑(∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))

State before:
i : ℕ
hi : i < 330
⊢ ↑((∏ x ∈ (Finset.range 330).erase i, (660 + x) * (1319 - x)) * ((660 + i) * (1319 - i))) /
      ((660 + ↑i) * (1319 - ↑i)) =
    ↑(∏ j ∈ (Finset.range 330).erase i, (660 + j) * (1319 - j))
Tactic:
push_cast
State after:
i : ℕ
hi : i < 330
⊢ (∏ 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)

State before:
i : ℕ
hi : i < 330
⊢ (∏ 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)
Tactic:
have h1 : (((1319 - i):ℕ):ℚ) = 1319 - (i:ℚ) := by
  have : i ≤ 1319 := by omega
  simp_all only [Nat.cast_sub, Nat.cast_ofNat]
State after:
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)

State before:
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)
Tactic:
rw [h1, mul_div_assoc]
State after:
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)

State before:
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)
Tactic:
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
State after:
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)

State before:
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)
Tactic:
rw [h2, mul_one]
State after:
no goals

State before:
i : ℕ
hi : i < 330
⊢ ↑(1319 - i) = 1319 - ↑i
Tactic:
have : i ≤ 1319 := by omega
State after:
i : ℕ
hi : i < 330
this : i ≤ 1319
⊢ ↑(1319 - i) = 1319 - ↑i

State before:
i : ℕ
hi : i < 330
this : i ≤ 1319
⊢ ↑(1319 - i) = 1319 - ↑i
Tactic:
simp_all only [Nat.cast_sub, Nat.cast_ofNat]
State after:
no goals

State before:
i : ℕ
hi : i < 330
⊢ i ≤ 1319
Tactic:
omega
State after:
no goals

State before:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
⊢ (660 + ↑i) * (1319 - ↑i) / ((660 + ↑i) * (1319 - ↑i)) = 1
Tactic:
have h3 : (660 + (i:ℚ)) * (1319 - (i:ℚ)) ≠ 0 := by
  have h5 : (i: ℚ) < 330 := by norm_cast
  nlinarith
State after:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
h3 : (660 + ↑i) * (1319 - ↑i) ≠ 0
⊢ (660 + ↑i) * (1319 - ↑i) / ((660 + ↑i) * (1319 - ↑i)) = 1

State before:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
h3 : (660 + ↑i) * (1319 - ↑i) ≠ 0
⊢ (660 + ↑i) * (1319 - ↑i) / ((660 + ↑i) * (1319 - ↑i)) = 1
Tactic:
exact div_self h3
State after:
no goals

State before:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
⊢ (660 + ↑i) * (1319 - ↑i) ≠ 0
Tactic:
have h5 : (i: ℚ) < 330 := by norm_cast
State after:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
h5 : ↑i < 330
⊢ (660 + ↑i) * (1319 - ↑i) ≠ 0

State before:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
h5 : ↑i < 330
⊢ (660 + ↑i) * (1319 - ↑i) ≠ 0
Tactic:
nlinarith
State after:
no goals

State before:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
⊢ ↑i < 330
Tactic:
norm_cast
State after:
no goals