internlm/Lean-Github huggingface dataset:
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * 5 ^ pn.succ * 2 = t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * 5 ^ pn * 10
Tactic:
rw[pow_succ]
Proof state after:
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * (5 ^ pn * 5) * 2 = t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * 5 ^ pn * 10
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * (5 ^ pn * 5) * 2 = t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * 5 ^ pn * 10
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5) = 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)
Tactic:
repeat rw[pow_succ]; ring_nf
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ t * 2 ^ pn * 4 + k5 * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 8 =
    t * 2 ^ pn.succ.succ + k5 * 2 ^ pn.succ.succ + 2 ^ pn.succ.succ * 5 ^ pn * 2
Tactic:
rw[pow_succ]
Proof state after:
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ t * 2 ^ pn * 4 + k5 * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 8 =
    t * (2 ^ (pn + 1) * 2) + k5 * (2 ^ (pn + 1) * 2) + 2 ^ (pn + 1) * 2 * 5 ^ pn * 2
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ t * 2 ^ pn * 4 + k5 * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 8 =
    t * (2 ^ (pn + 1) * 2) + k5 * (2 ^ (pn + 1) * 2) + 2 ^ (pn + 1) * 2 * 5 ^ pn * 2
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
k' : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
⊢ 0 < k'
Tactic:
cases k'
Proof state after:
case zero
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ 0 < 0

case succ
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
n✝ : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * (n✝ + 1)
⊢ 0 < n✝ + 1
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
case zero
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ 0 < 0
Tactic:
exfalso
Proof state after:
case zero
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ False
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
case zero
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ False
Tactic:
have hzz := prepend_one_pos (2 ^ pn.succ * ↑pk)
Proof state after:
case zero
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
hzz : 0 < prepend_one (2 ^ pn.succ * ↑pk)
⊢ False
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
case zero
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
hzz : 0 < prepend_one (2 ^ pn.succ * ↑pk)
⊢ False
Tactic:
rw[Nat.mul_zero] at hk'
Proof state after:
case zero
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 0
hzz : 0 < prepend_one (2 ^ pn.succ * ↑pk)
⊢ False
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
case zero
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 0
hzz : 0 < prepend_one (2 ^ pn.succ * ↑pk)
⊢ False
Tactic:
omega
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
case succ
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
n✝ : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * (n✝ + 1)
⊢ 0 < n✝ + 1
Tactic:
exact Nat.succ_pos _
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
case h.left
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
k' : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (prepend_one (2 ^ pn.succ * ↑pk))).length = (pn + 1).succ
Tactic:
rw [prepend_one_eq_append]
Proof state after:
case h.left
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
k' : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (2 ^ pn.succ * ↑pk) ++ [1]).length = (pn + 1).succ
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
case h.left
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
k' : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (2 ^ pn.succ * ↑pk) ++ [1]).length = (pn + 1).succ
Tactic:
rw [List.length_append, List.length_singleton, hpk1]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof state before:
case h.right
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t + 1
k' : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ all_one_or_two (Nat.digits 10 (prepend_one (2 ^ pn.succ * ↑pk)))
Tactic:
exact prepend_one_all_one_or_two _ hpk2
Proof state after:
no goals
Theorem: Imo1994P1.tedious
Proof state before:
m : ℕ
k : Fin (m + 1)
⊢ m - (m + (m + 1 - ↑k)) % (m + 1) = ↑k
Tactic:
cases' k with k hk
Proof state after:
case mk
m k : ℕ
hk : k < m + 1
⊢ m - (m + (m + 1 - ↑⟨k, hk⟩)) % (m + 1) = ↑⟨k, hk⟩
Theorem: Imo1994P1.tedious
Proof state before:
case mk
m k : ℕ
hk : k < m + 1
⊢ m - (m + (m + 1 - ↑⟨k, hk⟩)) % (m + 1) = ↑⟨k, hk⟩
Tactic:
rw [Nat.lt_succ_iff, le_iff_exists_add] at hk
Proof state after:
case mk
m k : ℕ
hk✝ : k < m + 1
hk : ∃ c, m = k + c
⊢ m - (m + (m + 1 - ↑⟨k, hk✝⟩)) % (m + 1) = ↑⟨k, hk✝⟩
Theorem: Imo1994P1.tedious
Proof state before:
case mk
m k : ℕ
hk✝ : k < m + 1
hk : ∃ c, m = k + c
⊢ m - (m + (m + 1 - ↑⟨k, hk✝⟩)) % (m + 1) = ↑⟨k, hk✝⟩
Tactic:
rcases hk with ⟨c, rfl⟩
Proof state after:
case mk.intro
k c : ℕ
hk : k < k + c + 1
⊢ k + c - (k + c + (k + c + 1 - ↑⟨k, hk⟩)) % (k + c + 1) = ↑⟨k, hk⟩
Theorem: Imo1994P1.tedious
Proof state before:
case mk.intro
k c : ℕ
hk : k < k + c + 1
⊢ k + c - (k + c + (k + c + 1 - ↑⟨k, hk⟩)) % (k + c + 1) = ↑⟨k, hk⟩
Tactic:
have : k + c + (k + c + 1 - k) = c + (k + c + 1) := by
  simp only [add_assoc, add_tsub_cancel_left, add_left_comm]
Proof state after:
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ k + c - (k + c + (k + c + 1 - ↑⟨k, hk⟩)) % (k + c + 1) = ↑⟨k, hk⟩
Theorem: Imo1994P1.tedious
Proof state before:
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ k + c - (k + c + (k + c + 1 - ↑⟨k, hk⟩)) % (k + c + 1) = ↑⟨k, hk⟩
Tactic:
rw [Fin.val_mk, this, Nat.add_mod_right, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
Proof state after:
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ c < k + c + 1
Theorem: Imo1994P1.tedious
Proof state before:
case mk.intro
k c : ℕ
hk : k < k + c + 1
this : k + c + (k + c + 1 - k) = c + (k + c + 1)
⊢ c < k + c + 1
Tactic:
omega
Proof state after:
no goals
Theorem: Imo1994P1.tedious
Proof state before:
k c : ℕ
hk : k < k + c + 1
⊢ k + c + (k + c + 1 - k) = c + (k + c + 1)
Tactic:
simp only [add_assoc, add_tsub_cancel_left, add_left_comm]
Proof state after:
no goals
Theorem: Imo1964P1.imo_1964_p1b'
Proof state before:
⊢ (2 ^ 2 + 1) % 7 ≠ 0
Tactic:
decide
Proof state after:
no goals
Theorem: Imo1964P1.imo_1964_p1b'
Proof state before:
n : ℕ
⊢ (2 ^ (n + 3) + 1) % 7 ≠ 0
Tactic:
rw [pow_add, Nat.add_mod, Nat.mul_mod, show 2 ^ 3 % 7 = 1 by rfl]
Proof state after:
n : ℕ
⊢ (2 ^ n % 7 * 1 % 7 + 1 % 7) % 7 ≠ 0
Theorem: Imo1964P1.imo_1964_p1b'
Proof state before:
n : ℕ
⊢ (2 ^ n % 7 * 1 % 7 + 1 % 7) % 7 ≠ 0
Tactic:
simp [imo_1964_p1b' n]
Proof state after:
no goals
Theorem: Imo1964P1.imo_1964_p1b'
Proof state before:
n : ℕ
⊢ 2 ^ 3 % 7 = 1
Tactic:
rfl
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)
⊢ ∑ i ∈ Finset.range 1319, (-1) ^ i / (↑i + 1) =
    ∑ i ∈ Finset.range 1319, 1 / (↑i + 1) - 2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
Tactic:
rw [←h2]
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)
⊢ ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 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)
⊢ ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
Tactic:
let g : ℕ ↪ ℕ :=
  ⟨fun x ↦ 2 * x + 1,
   by intro a b hab; dsimp at hab; omega⟩
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' := ⋯ }
⊢ ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 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)
⊢ ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
Tactic:
have h5 : ∑ i ∈ Finset.range 659, 1 / (2 * ((i:ℚ) + 1))
     = ∑ i ∈ Finset.range 659, (1 / (((g i):ℚ) + 1)) := by
  apply Finset.sum_congr rfl
  intro x _
  field_simp [g]; ring
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)
⊢ ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 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)
⊢ ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
Tactic:
have h6 := Finset.sum_map (Finset.range 659) g (fun j ↦ 1 / ((j:ℚ) + 1))
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)
⊢ ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 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)
⊢ ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
Tactic:
have h3 :
  ∑ x ∈ Finset.filter (fun x ↦ ¬Even x) (Finset.range 1319),
   1 / ((x:ℚ) + 1) =
    ∑ i ∈ Finset.range 659, 1 / (2 * ((i:ℚ) + 1)) := by
  rw [h5]
  rw [←h6, h4]
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) =
    ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 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) =
    ∑ 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) -
      2 * ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
Tactic:
rw [h3, two_mul, add_sub_add_right_eq_sub]
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) =
    ∑ x ∈ Finset.filter (fun x => Even x) (Finset.range 1319), 1 / (↑x + 1) - ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 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) =
    ∑ x ∈ Finset.filter (fun x => Even x) (Finset.range 1319), 1 / (↑x + 1) - ∑ i ∈ Finset.range 659, 1 / (2 * (↑i + 1))
Tactic:
rw [←h3, ←h4, h6, ←h5, ←h3]
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) =
    ∑ 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)
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) =
    ∑ 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:
have 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) := by
  apply Finset.sum_congr rfl
  intro x hx
  rw [Finset.mem_filter] at hx
  have h9: (-1 : ℚ)^x = 1 := Even.neg_one_pow hx.2
  rw [h9]
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) =
    ∑ 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)