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))
h7 :
  ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), 1 / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1)
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ 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)
Tactic:
rw [h7]
Proof state after:
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))
h7 :
  ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), 1 / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1)
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) -
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1)
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))
h7 :
  ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), 1 / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1)
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) -
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1)
Tactic:
clear h7
Proof state after:
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))
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) -
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1)
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))
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) -
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), 1 / (↑x + 1)
Tactic:
rw [Rat.sub_eq_add_neg, ←Finset.sum_neg_distrib]
Proof state after:
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))
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) +
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), -(1 / (↑x + 1))
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))
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) +
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), -(1 / (↑x + 1))
Tactic:
have h10 : ∑ 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 / ((x:ℚ) + 1) := by
  apply Finset.sum_congr rfl
  intro x hx
  rw [Finset.mem_filter] at hx
  have h9: (-1 : ℚ)^x = -1 := Odd.neg_one_pow (Nat.odd_iff_not_even.mpr hx.2)
  rw [h9]
  field_simp
Proof state after:
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))
h10 :
  ∑ 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 / (↑x + 1)
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) +
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), -(1 / (↑x + 1))
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))
h10 :
  ∑ 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 / (↑x + 1)
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.filter (fun x => Even x) (Finset.range 1319), (-1) ^ i / (↑i + 1) +
      ∑ x ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319), -(1 / (↑x + 1))
Tactic:
rw [h10, Finset.sum_filter_add_sum_filter_not]
Proof state after:
no goals
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)
⊢ Function.Injective fun x => 2 * x + 1
Tactic:
intro a b hab
Proof state after:
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)
a b : ℕ
hab : (fun x => 2 * x + 1) a = (fun x => 2 * x + 1) b
⊢ a = b
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)
a b : ℕ
hab : (fun x => 2 * x + 1) a = (fun x => 2 * x + 1) b
⊢ a = b
Tactic:
dsimp at hab
Proof state after:
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)
a b : ℕ
hab : 2 * a + 1 = 2 * b + 1
⊢ a = b
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)
a b : ℕ
hab : 2 * a + 1 = 2 * b + 1
⊢ a = b
Tactic:
omega
Proof state after:
no goals
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' := ⋯ }
⊢ Finset.map g (Finset.range 659) = Finset.filter (fun x => ¬Even x) (Finset.range 1319)
Tactic:
ext a
Proof state after:
case a
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' := ⋯ }
a : ℕ
⊢ a ∈ Finset.map g (Finset.range 659) ↔ a ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319)
Theorem: Imo1979P1.lemma3
Proof state before:
case a
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' := ⋯ }
a : ℕ
⊢ a ∈ Finset.map g (Finset.range 659) ↔ a ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319)
Tactic:
unfold_let g
Proof state after:
case a
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' := ⋯ }
a : ℕ
⊢ a ∈ Finset.map { toFun := fun x => 2 * x + 1, inj' := ⋯ } (Finset.range 659) ↔
    a ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319)
Theorem: Imo1979P1.lemma3
Proof state before:
case a
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' := ⋯ }
a : ℕ
⊢ a ∈ Finset.map { toFun := fun x => 2 * x + 1, inj' := ⋯ } (Finset.range 659) ↔
    a ∈ Finset.filter (fun x => ¬Even x) (Finset.range 1319)
Tactic:
rw [Finset.mem_map, Function.Embedding.coeFn_mk,
    Finset.mem_filter, Finset.mem_range]
Proof state after:
case a
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' := ⋯ }
a : ℕ
⊢ (∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a) ↔ a < 1319 ∧ ¬Even a
Theorem: Imo1979P1.lemma3
Proof state before:
case a
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' := ⋯ }
a : ℕ
⊢ (∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a) ↔ a < 1319 ∧ ¬Even a
Tactic:
constructor
Proof state after:
case a.mp
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' := ⋯ }
a : ℕ
⊢ (∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a) → a < 1319 ∧ ¬Even a

case a.mpr
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' := ⋯ }
a : ℕ
⊢ a < 1319 ∧ ¬Even a → ∃ a_2 ∈ Finset.range 659, 2 * a_2 + 1 = a
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mp
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' := ⋯ }
a : ℕ
⊢ (∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a) → a < 1319 ∧ ¬Even a
Tactic:
intro ha
Proof state after:
case a.mp
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' := ⋯ }
a : ℕ
ha : ∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a
⊢ a < 1319 ∧ ¬Even a
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mp
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' := ⋯ }
a : ℕ
ha : ∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a
⊢ a < 1319 ∧ ¬Even a
Tactic:
obtain ⟨b, hb1, hb2⟩ := ha
Proof state after:
case a.mp.intro.intro
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' := ⋯ }
a b : ℕ
hb1 : b ∈ Finset.range 659
hb2 : 2 * b + 1 = a
⊢ a < 1319 ∧ ¬Even a
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mp.intro.intro
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' := ⋯ }
a b : ℕ
hb1 : b ∈ Finset.range 659
hb2 : 2 * b + 1 = a
⊢ a < 1319 ∧ ¬Even a
Tactic:
rw [Finset.mem_range] at hb1
Proof state after:
case a.mp.intro.intro
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' := ⋯ }
a b : ℕ
hb1 : b < 659
hb2 : 2 * b + 1 = a
⊢ a < 1319 ∧ ¬Even a
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mp.intro.intro
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' := ⋯ }
a b : ℕ
hb1 : b < 659
hb2 : 2 * b + 1 = a
⊢ a < 1319 ∧ ¬Even a
Tactic:
rw [←hb2]
Proof state after:
case a.mp.intro.intro
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' := ⋯ }
a b : ℕ
hb1 : b < 659
hb2 : 2 * b + 1 = a
⊢ 2 * b + 1 < 1319 ∧ ¬Even (2 * b + 1)
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mp.intro.intro
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' := ⋯ }
a b : ℕ
hb1 : b < 659
hb2 : 2 * b + 1 = a
⊢ 2 * b + 1 < 1319 ∧ ¬Even (2 * b + 1)
Tactic:
constructor
Proof state after:
case a.mp.intro.intro.left
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' := ⋯ }
a b : ℕ
hb1 : b < 659
hb2 : 2 * b + 1 = a
⊢ 2 * b + 1 < 1319

case a.mp.intro.intro.right
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' := ⋯ }
a b : ℕ
hb1 : b < 659
hb2 : 2 * b + 1 = a
⊢ ¬Even (2 * b + 1)
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mp.intro.intro.left
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' := ⋯ }
a b : ℕ
hb1 : b < 659
hb2 : 2 * b + 1 = a
⊢ 2 * b + 1 < 1319
Tactic:
omega
Proof state after:
no goals
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mp.intro.intro.right
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' := ⋯ }
a b : ℕ
hb1 : b < 659
hb2 : 2 * b + 1 = a
⊢ ¬Even (2 * b + 1)
Tactic:
exact Nat.odd_iff_not_even.mp ⟨b, rfl⟩
Proof state after:
no goals
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mpr
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' := ⋯ }
a : ℕ
⊢ a < 1319 ∧ ¬Even a → ∃ a_2 ∈ Finset.range 659, 2 * a_2 + 1 = a
Tactic:
rintro ⟨ha1, ha2⟩
Proof state after:
case a.mpr.intro
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' := ⋯ }
a : ℕ
ha1 : a < 1319
ha2 : ¬Even a
⊢ ∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mpr.intro
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' := ⋯ }
a : ℕ
ha1 : a < 1319
ha2 : ¬Even a
⊢ ∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a
Tactic:
have h5 : Odd a := Nat.odd_iff_not_even.mpr ha2
Proof state after:
case a.mpr.intro
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' := ⋯ }
a : ℕ
ha1 : a < 1319
ha2 : ¬Even a
h5 : Odd a
⊢ ∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mpr.intro
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' := ⋯ }
a : ℕ
ha1 : a < 1319
ha2 : ¬Even a
h5 : Odd a
⊢ ∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a
Tactic:
obtain ⟨r, hr⟩ := h5
Proof state after:
case a.mpr.intro.intro
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' := ⋯ }
a : ℕ
ha1 : a < 1319
ha2 : ¬Even a
r : ℕ
hr : a = 2 * r + 1
⊢ ∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a
Theorem: Imo1979P1.lemma3
Proof state before:
case a.mpr.intro.intro
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' := ⋯ }
a : ℕ
ha1 : a < 1319
ha2 : ¬Even a
r : ℕ
hr : a = 2 * r + 1
⊢ ∃ a_1 ∈ Finset.range 659, 2 * a_1 + 1 = a
Tactic:
use r
Proof state after:
case h
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' := ⋯ }
a : ℕ
ha1 : a < 1319
ha2 : ¬Even a
r : ℕ
hr : a = 2 * r + 1
⊢ r ∈ Finset.range 659 ∧ 2 * r + 1 = a