internlm/Lean-Github huggingface dataset:
Theorem: Imo1979P1.lemma3
Proof state before:
h2 :
  ∑ x ∈ Finset.filter (fun x => Even x) (Finset.range 1319), 1 / (↑x + 1) +
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1) =
    ∑ x ∈ Finset.range 1319, 1 / (↑x + 1)
g : ℕ ↪ ℕ := { toFun := fun x => 2 * x + 1, inj' := ⋯ }
h4 : Finset.map g (Finset.range 659) = Finset.filter (fun x => ¬Even x) (Finset.range 1319)
h5 : ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1)) = ∑ i ∈ Finset.range 659, 1 / (↑(g i) + 1)
h6 : ∑ x ∈ Finset.map g (Finset.range 659), 1 / (↑x + 1) = ∑ x ∈ Finset.range 659, 1 / (↑(g x) + 1)
h3 :
  ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1) = ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
x : ℕ
hx : x ∈ Finset.range 1319 ∧ ¬Even x
h9 : (-1) ^ x = -1
⊢ -(1 / (↑x + 1)) = -1 / (↑x + 1)
Tactic:
field_simp
Proof state after:
no goals
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
have h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i =
          (∑ i ∈ Finset.Ico n (n + m), f i) +
          (∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i) := by
  have hmn : n ≤ n + m := Nat.le_add_right n m
  have hnk : n + m ≤ n + 2 * m := by omega
  exact (Finset.sum_Ico_consecutive (fun i ↦ f i) hmn hnk).symm
Proof state after:
n m : ℕ
f : ℕ → ℚ
h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
rw [h1]
Proof state after:
n m : ℕ
f : ℕ → ℚ
h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
⊢ ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
h1 : ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
⊢ ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
clear h1
Proof state after:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
simp only [Finset.sum_Ico_eq_sum_range, add_tsub_cancel_left]
Proof state after:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ x ∈ Finset.range m, f (n + x) + ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ x ∈ Finset.range m, f (n + x) + ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
Tactic:
rw [Finset.sum_add_distrib, add_right_inj]
Proof state after:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
Tactic:
rw [show n + 2 * m - (n + m) = m by omega]
Proof state after:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
Tactic:
have h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i)) := by
  intro i hi
  rw [Finset.mem_range] at hi
  apply congr_arg
  omega
Proof state after:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
Tactic:
rw [Finset.sum_congr rfl h2]
Proof state after:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))
Tactic:
let g i := f (n + m + i)
Proof state after:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
g : ℕ → ℚ := fun i => f (n + m + i)
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
h2 : ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
g : ℕ → ℚ := fun i => f (n + m + i)
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + m + (m - 1 - x))
Tactic:
rw [Finset.sum_range_reflect g]
Proof state after:
no goals
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
Tactic:
have hmn : n ≤ n + m := Nat.le_add_right n m
Proof state after:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
Tactic:
have hnk : n + m ≤ n + 2 * m := by omega
Proof state after:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
hnk : n + m ≤ n + 2 * m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
hnk : n + m ≤ n + 2 * m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
Tactic:
exact (Finset.sum_Ico_consecutive (fun i ↦ f i) hmn hnk).symm
Proof state after:
no goals
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
⊢ n + m ≤ n + 2 * m
Tactic:
omega
Proof state after:
no goals
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
⊢ n + 2 * m - (n + m) = m
Tactic:
omega
Proof state after:
no goals
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
⊢ ∀ i ∈ Finset.range m, f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
Tactic:
intro i hi
Proof state after:
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i ∈ Finset.range m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i ∈ Finset.range m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
Tactic:
rw [Finset.mem_range] at hi
Proof state after:
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i < m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
Theorem: Imo1979P1.lemma4
Proof state before:
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i < m
⊢ f (n + (2 * m - 1 - i)) = f (n + m + (m - 1 - i))
Tactic:
apply congr_arg
Proof state after:
case h
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i < m
⊢ n + (2 * m - 1 - i) = n + m + (m - 1 - i)
Theorem: Imo1979P1.lemma4
Proof state before:
case h
n m : ℕ
f : ℕ → ℚ
i : ℕ
hi : i < m
⊢ n + (2 * m - 1 - i) = n + m + (m - 1 - i)
Tactic:
omega
Proof state after:
no goals
Theorem: Imo1979P1.lemma9'
Proof 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]
Proof 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))
Theorem: Imo1979P1.lemma9'
Proof 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
Proof 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))
Theorem: Imo1979P1.lemma9'
Proof 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
Proof 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)
Theorem: Imo1979P1.lemma9'
Proof 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]
Proof 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)
Theorem: Imo1979P1.lemma9'
Proof 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]
Proof 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)
Theorem: Imo1979P1.lemma9'
Proof 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
Proof 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)
Theorem: Imo1979P1.lemma9'
Proof 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]
Proof state after:
no goals
Theorem: Imo1979P1.lemma9'
Proof state before:
i : ℕ
hi : i < 330
⊢ ↑(1319 - i) = 1319 - ↑i
Tactic:
have : i ≤ 1319 := by omega
Proof state after:
i : ℕ
hi : i < 330
this : i ≤ 1319
⊢ ↑(1319 - i) = 1319 - ↑i
Theorem: Imo1979P1.lemma9'
Proof state before:
i : ℕ
hi : i < 330
this : i ≤ 1319
⊢ ↑(1319 - i) = 1319 - ↑i
Tactic:
simp_all only [Nat.cast_sub, Nat.cast_ofNat]
Proof state after:
no goals
Theorem: Imo1979P1.lemma9'
Proof state before:
i : ℕ
hi : i < 330
⊢ i ≤ 1319
Tactic:
omega
Proof state after:
no goals
Theorem: Imo1979P1.lemma9'
Proof 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
Proof 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
Theorem: Imo1979P1.lemma9'
Proof 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
Proof state after:
no goals
Theorem: Imo1979P1.lemma9'
Proof state before:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
⊢ (660 + ↑i) * (1319 - ↑i) ≠ 0
Tactic:
have h5 : (i: ℚ) < 330 := by norm_cast
Proof state after:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
h5 : ↑i < 330
⊢ (660 + ↑i) * (1319 - ↑i) ≠ 0
Theorem: Imo1979P1.lemma9'
Proof state before:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
h5 : ↑i < 330
⊢ (660 + ↑i) * (1319 - ↑i) ≠ 0
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Imo1979P1.lemma9'
Proof state before:
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
⊢ ↑i < 330
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Imo1979P1.lemma9
Proof 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]
Proof 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))
Theorem: Imo1979P1.lemma9
Proof 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']
Proof 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))
Theorem: Imo1979P1.lemma9
Proof 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
Proof 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)
Theorem: Imo1979P1.lemma9
Proof 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
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff
Proof state before:
x A : ℝ
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
cases le_or_lt (1 / 2) x with
| inl hx =>
  have hx' : 0 ≤ 2 * x - 1 := by linarith
  have h₁ : x + sqrt (2 * x - 1) = (sqrt (2 * x - 1) + 1) ^ 2 / 2 := by
    rw [add_sq, sq_sqrt hx']; field_simp; ring
  have h₂ : x - sqrt (2 * x - 1) = (sqrt (2 * x - 1) - 1) ^ 2 / 2 := by
    rw [sub_sq, sq_sqrt hx']; field_simp; ring
  simp only [IsGood, *, div_nonneg (sq_nonneg _) (zero_le_two (α := ℝ)), sqrt_div (sq_nonneg _),
    and_true]
  rw [sqrt_sq, sqrt_sq_eq_abs] <;> [skip; positivity]
  field_simp
| inr hx =>
  have : 2 * x - 1 < 0 := by linarith
  simp only [IsGood, this.not_le, hx.not_le]; simp
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff
Proof state before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
have hx' : 0 ≤ 2 * x - 1 := by linarith
Proof state after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Theorem: Imo1959P2.isGood_iff
Proof state before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
have h₁ : x + sqrt (2 * x - 1) = (sqrt (2 * x - 1) + 1) ^ 2 / 2 := by
  rw [add_sq, sq_sqrt hx']; field_simp; ring
Proof state after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Theorem: Imo1959P2.isGood_iff
Proof state before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
have h₂ : x - sqrt (2 * x - 1) = (sqrt (2 * x - 1) - 1) ^ 2 / 2 := by
  rw [sub_sq, sq_sqrt hx']; field_simp; ring
Proof state after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Theorem: Imo1959P2.isGood_iff
Proof state before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
simp only [IsGood, *, div_nonneg (sq_nonneg _) (zero_le_two (α := ℝ)), sqrt_div (sq_nonneg _),
  and_true]
Proof state after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ √((√(2 * x - 1) + 1) ^ 2) / √2 + √((√(2 * x - 1) - 1) ^ 2) / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2
Theorem: Imo1959P2.isGood_iff
Proof state before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ √((√(2 * x - 1) + 1) ^ 2) / √2 + √((√(2 * x - 1) - 1) ^ 2) / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2
Tactic:
rw [sqrt_sq, sqrt_sq_eq_abs] <;> [skip; positivity]
Proof state after:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ (√(2 * x - 1) + 1) / √2 + |√(2 * x - 1) - 1| / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2
Theorem: Imo1959P2.isGood_iff
Proof state before:
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ (√(2 * x - 1) + 1) / √2 + |√(2 * x - 1) - 1| / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2
Tactic:
field_simp
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff
Proof state before:
x A : ℝ
hx : 1 / 2 ≤ x
⊢ 0 ≤ 2 * x - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff
Proof state before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
Tactic:
rw [add_sq, sq_sqrt hx']
Proof state after:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ x + √(2 * x - 1) = (2 * x - 1 + 2 * √(2 * x - 1) * 1 + 1 ^ 2) / 2
Theorem: Imo1959P2.isGood_iff
Proof state before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ x + √(2 * x - 1) = (2 * x - 1 + 2 * √(2 * x - 1) * 1 + 1 ^ 2) / 2
Tactic:
field_simp
Proof state after:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ (x + √(2 * x - 1)) * 2 = 2 * x - 1 + 2 * √(2 * x - 1) + 1
Theorem: Imo1959P2.isGood_iff
Proof state before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
⊢ (x + √(2 * x - 1)) * 2 = 2 * x - 1 + 2 * √(2 * x - 1) + 1
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff
Proof state before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
Tactic:
rw [sub_sq, sq_sqrt hx']
Proof state after:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ x - √(2 * x - 1) = (2 * x - 1 - 2 * √(2 * x - 1) * 1 + 1 ^ 2) / 2
Theorem: Imo1959P2.isGood_iff
Proof state before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ x - √(2 * x - 1) = (2 * x - 1 - 2 * √(2 * x - 1) * 1 + 1 ^ 2) / 2
Tactic:
field_simp
Proof state after:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ (x - √(2 * x - 1)) * 2 = 2 * x - 1 - 2 * √(2 * x - 1) + 1
Theorem: Imo1959P2.isGood_iff
Proof state before:
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
⊢ (x - √(2 * x - 1)) * 2 = 2 * x - 1 - 2 * √(2 * x - 1) + 1
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff
Proof state before:
case inr
x A : ℝ
hx : x < 1 / 2
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
have : 2 * x - 1 < 0 := by linarith
Proof state after:
case inr
x A : ℝ
hx : x < 1 / 2
this : 2 * x - 1 < 0
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Theorem: Imo1959P2.isGood_iff
Proof state before:
case inr
x A : ℝ
hx : x < 1 / 2
this : 2 * x - 1 < 0
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
Tactic:
simp only [IsGood, this.not_le, hx.not_le]
Proof state after:
case inr
x A : ℝ
hx : x < 1 / 2
this : 2 * x - 1 < 0
⊢ √(x + √(2 * x - 1)) + √(x - √(2 * x - 1)) = A ∧ False ∧ 0 ≤ x + √(2 * x - 1) ∧ 0 ≤ x - √(2 * x - 1) ↔
    √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ False
Theorem: Imo1959P2.isGood_iff
Proof state before:
case inr
x A : ℝ
hx : x < 1 / 2
this : 2 * x - 1 < 0
⊢ √(x + √(2 * x - 1)) + √(x - √(2 * x - 1)) = A ∧ False ∧ 0 ≤ x + √(2 * x - 1) ∧ 0 ≤ x - √(2 * x - 1) ↔
    √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ False
Tactic:
simp
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff
Proof state before:
x A : ℝ
hx : x < 1 / 2
⊢ 2 * x - 1 < 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1959P2.sqrt_two_mul_sub_one_le_one
Proof state before:
x A : ℝ
⊢ √(2 * x - 1) ≤ 1 ↔ x ≤ 1
Tactic:
simp [sqrt_le_iff, ← two_mul]
Proof state after:
no goals
Theorem: Imo1959P2.isGood_iff_eq_sqrt_two
Proof state before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
⊢ IsGood x A ↔ A = √2
Tactic:
have : sqrt (2 * x - 1) ≤ 1 := sqrt_two_mul_sub_one_le_one.2 hx.2
Proof state after:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ IsGood x A ↔ A = √2
Theorem: Imo1959P2.isGood_iff_eq_sqrt_two
Proof state before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ IsGood x A ↔ A = √2
Tactic:
simp only [isGood_iff, hx.1, abs_sub_comm _ (1 : ℝ), abs_of_nonneg (sub_nonneg.2 this), and_true]
Proof state after:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = A * √2 ↔ A = √2
Theorem: Imo1959P2.isGood_iff_eq_sqrt_two
Proof state before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = A * √2 ↔ A = √2
Tactic:
suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert this using 2; ring
Proof state after:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ 2 = A * √2 ↔ A = √2
Theorem: Imo1959P2.isGood_iff_eq_sqrt_two
Proof state before:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ 2 = A * √2 ↔ A = √2
Tactic:
rw [← div_eq_iff, div_sqrt, eq_comm]
Proof state after:
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √2 ≠ 0