internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
k : ℕ
⊢ 2 ^ (Nat.zero + 1) ∣ f^[k] M - 3
Tactic:
rw [Int.dvd_iff_emod_eq_zero, Nat.zero_add, pow_one,
  ← Int.even_iff, Int.even_sub', Int.odd_iff_not_even,
  Int.even_iff, ← Int.dvd_iff_emod_eq_zero]
Proof state after:
case refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
k : ℕ
⊢ ¬2 ∣ f^[k] M ↔ Odd 3
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
k : ℕ
⊢ ¬2 ∣ f^[k] M ↔ Odd 3
Tactic:
exact iff_of_true (h k) (Int.odd_iff.mpr rfl)
Proof state after:
no goals
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n.succ + 1) ∣ f^[k] M - 3
Tactic:
rw [pow_succ', pow_succ']
Proof state after:
case refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * (2 * 2 ^ n) ∣ f^[k] M - 3
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * (2 * 2 ^ n) ∣ f^[k] M - 3
Tactic:
refine main_claim ?_ ?_
Proof state after:
case refine_2.refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * 2 ^ n ∣ f^[k] M - 3

case refine_2.refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * 2 ^ n ∣ f (f^[k] M) - 3
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2.refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * 2 ^ n ∣ f^[k] M - 3
Tactic:
rw [← pow_succ']
Proof state after:
case refine_2.refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n + 1) ∣ f^[k] M - 3
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2.refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n + 1) ∣ f^[k] M - 3
Tactic:
exact h0 k
Proof state after:
no goals
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2.refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 * 2 ^ n ∣ f (f^[k] M) - 3
Tactic:
rw [← pow_succ', ← f.iterate_succ_apply']
Proof state after:
case refine_2.refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n + 1) ∣ f^[k.succ] M - 3
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2.refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n + 1) ∣ f^[k.succ] M - 3
Tactic:
exact h0 (k + 1)
Proof state after:
no goals
Theorem: IMOSL.IMO2009N2.Even_iff_bodd
Proof state before:
k : ℕ
⊢ Even k ↔ k.bodd = false
Tactic:
rw [Nat.even_iff, Nat.mod_two_of_bodd, Bool.cond_eq_ite,
  Nat.one_ne_zero.ite_eq_right_iff, Bool.bool_iff_false]
Proof state after:
no goals
Theorem: IMOSL.IMO2009N2.xor_eq_false_iff_eq
Proof state before:
a b : Bool
⊢ xor a b = false ↔ a = b
Tactic:
rw [← Bool.bool_iff_false, Bool.xor_iff_ne, not_not]
Proof state after:
no goals
Theorem: IMOSL.IMO2009N2.final_solution_part1
Proof state before:
N : ℕ
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Tactic:
let f : ℕ → Fin N → Bool := λ a k ↦ (Ω (a.succ + k)).bodd
Proof state after:
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Theorem: IMOSL.IMO2009N2.final_solution_part1
Proof state before:
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Tactic:
have h : ¬f.Injective := not_injective_infinite_finite f
Proof state after:
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
h : ¬Function.Injective f
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Theorem: IMOSL.IMO2009N2.final_solution_part1
Proof state before:
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
h : ¬Function.Injective f
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Tactic:
rw [Function.Injective] at h
Proof state after:
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
h : ¬∀ ⦃a₁ a₂ : ℕ⦄, f a₁ = f a₂ → a₁ = a₂
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Theorem: IMOSL.IMO2009N2.final_solution_part1
Proof state before:
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
h : ¬∀ ⦃a₁ a₂ : ℕ⦄, f a₁ = f a₂ → a₁ = a₂
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Tactic:
simp_rw [not_forall] at h
Proof state after:
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
h : ∃ x x_1, ∃ (_ : f x = f x_1), ¬x = x_1
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Theorem: IMOSL.IMO2009N2.final_solution_part1
Proof state before:
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
h : ∃ x x_1, ∃ (_ : f x = f x_1), ¬x = x_1
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Tactic:
rcases h with ⟨a, b, h, h0⟩
Proof state after:
case intro.intro.intro
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
a b : ℕ
h : f a = f b
h0 : ¬a = b
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Theorem: IMOSL.IMO2009N2.final_solution_part1
Proof state before:
case intro.intro.intro
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
a b : ℕ
h : f a = f b
h0 : ¬a = b
⊢ ∃ a b, a ≠ b ∧ ∀ k < N, Even (Ω ((a + k) * (b + k)))
Tactic:
refine ⟨a.succ, b.succ, Nat.succ_ne_succ.mpr h0, λ k h1 ↦ ?_⟩
Proof state after:
case intro.intro.intro
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
a b : ℕ
h : f a = f b
h0 : ¬a = b
k : ℕ
h1 : k < N
⊢ Even (Ω ((a.succ + k) * (b.succ + k)))
Theorem: IMOSL.IMO2009N2.final_solution_part1
Proof state before:
case intro.intro.intro
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
a b : ℕ
h : f a = f b
h0 : ¬a = b
k : ℕ
h1 : k < N
⊢ Even (Ω ((a.succ + k) * (b.succ + k)))
Tactic:
have X (c : ℕ) : c.succ + k ≠ 0 := c.succ_add k ▸ (c + k).succ_ne_zero
Proof state after:
case intro.intro.intro
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
a b : ℕ
h : f a = f b
h0 : ¬a = b
k : ℕ
h1 : k < N
X : ∀ (c : ℕ), c.succ + k ≠ 0
⊢ Even (Ω ((a.succ + k) * (b.succ + k)))
Theorem: IMOSL.IMO2009N2.final_solution_part1
Proof state before:
case intro.intro.intro
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
a b : ℕ
h : f a = f b
h0 : ¬a = b
k : ℕ
h1 : k < N
X : ∀ (c : ℕ), c.succ + k ≠ 0
⊢ Even (Ω ((a.succ + k) * (b.succ + k)))
Tactic:
rw [Even_iff_bodd, cardFactors_mul (X _) (X _),
  Nat.bodd_add, xor_eq_false_iff_eq]
Proof state after:
case intro.intro.intro
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
a b : ℕ
h : f a = f b
h0 : ¬a = b
k : ℕ
h1 : k < N
X : ∀ (c : ℕ), c.succ + k ≠ 0
⊢ (Ω (a.succ + k)).bodd = (Ω (b.succ + k)).bodd
Theorem: IMOSL.IMO2009N2.final_solution_part1
Proof state before:
case intro.intro.intro
N : ℕ
f : ℕ → Fin N → Bool := fun a k => (Ω (a.succ + ↑k)).bodd
a b : ℕ
h : f a = f b
h0 : ¬a = b
k : ℕ
h1 : k < N
X : ∀ (c : ℕ), c.succ + k ≠ 0
⊢ (Ω (a.succ + k)).bodd = (Ω (b.succ + k)).bodd
Tactic:
exact congr_fun h ⟨k, h1⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2009N2.exists_lt_omega_bodd_ne_succ
Proof state before:
a : ℕ
⊢ ∃ b, a ≤ b ∧ (Ω b).bodd ≠ (Ω b.succ).bodd
Tactic:
by_contra h
Proof state after:
a : ℕ
h : ¬∃ b, a ≤ b ∧ (Ω b).bodd ≠ (Ω b.succ).bodd
⊢ False
Theorem: IMOSL.IMO2009N2.exists_lt_omega_bodd_ne_succ
Proof state before:
a : ℕ
h : ¬∃ b, a ≤ b ∧ (Ω b).bodd ≠ (Ω b.succ).bodd
⊢ False
Tactic:
rw [not_exists] at h
Proof state after:
a : ℕ
h : ∀ (x : ℕ), ¬(a ≤ x ∧ (Ω x).bodd ≠ (Ω x.succ).bodd)
⊢ False
Theorem: IMOSL.IMO2009N2.exists_lt_omega_bodd_ne_succ
Proof state before:
a : ℕ
h : ∀ (x : ℕ), ¬(a ≤ x ∧ (Ω x).bodd ≠ (Ω x.succ).bodd)
⊢ False
Tactic:
simp_rw [not_and, not_not] at h
Proof state after:
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
⊢ False
Theorem: IMOSL.IMO2009N2.exists_lt_omega_bodd_ne_succ
Proof state before:
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
⊢ False
Tactic:
rcases a.exists_infinite_primes with ⟨p, h0, h1⟩
Proof state after:
case intro.intro
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
p : ℕ
h0 : a ≤ p
h1 : p.Prime
⊢ False
Theorem: IMOSL.IMO2009N2.exists_lt_omega_bodd_ne_succ
Proof state before:
case intro.intro
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
p : ℕ
h0 : a ≤ p
h1 : p.Prime
⊢ False
Tactic:
apply absurd (eventually_const_of_map_succ_eq h
  p (p * p) h0 (h0.trans (Nat.le_mul_self p)))
Proof state after:
case intro.intro
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
p : ℕ
h0 : a ≤ p
h1 : p.Prime
⊢ ¬(Ω p).bodd = (Ω (p * p)).bodd
Theorem: IMOSL.IMO2009N2.exists_lt_omega_bodd_ne_succ
Proof state before:
case intro.intro
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
p : ℕ
h0 : a ≤ p
h1 : p.Prime
⊢ ¬(Ω p).bodd = (Ω (p * p)).bodd
Tactic:
rw [cardFactors_apply_prime h1, ← sq, cardFactors_apply_prime_pow h1]
Proof state after:
case intro.intro
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
p : ℕ
h0 : a ≤ p
h1 : p.Prime
⊢ ¬Nat.bodd 1 = Nat.bodd 2
Theorem: IMOSL.IMO2009N2.exists_lt_omega_bodd_ne_succ
Proof state before:
case intro.intro
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
p : ℕ
h0 : a ≤ p
h1 : p.Prime
⊢ ¬Nat.bodd 1 = Nat.bodd 2
Tactic:
trivial
Proof state after:
no goals
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
⊢ a = b
Tactic:
wlog h0 : a ≤ b
Proof state after:
case inr
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
this : ∀ {a b : ℕ}, (∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))) → a ≤ b → a = b
h0 : ¬a ≤ b
⊢ a = b

a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
h0 : a ≤ b
⊢ a = b
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
h0 : a ≤ b
⊢ a = b
Tactic:
rw [le_iff_exists_add] at h0
Proof state after:
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
h0 : ∃ c, b = a + c
⊢ a = b
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
h0 : ∃ c, b = a + c
⊢ a = b
Tactic:
rcases h0 with ⟨_ | c, rfl⟩
Proof state after:
case intro.zero
b : ℕ
h : ∀ (k : ℕ), Even (Ω ((b + k) * (b + k)))
⊢ b = b

case intro.succ
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
⊢ a = a + (c + 1)
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.zero
b : ℕ
h : ∀ (k : ℕ), Even (Ω ((b + k) * (b + k)))
⊢ b = b

case intro.succ
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
⊢ a = a + (c + 1)
Tactic:
rfl
Proof state after:
case intro.succ
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
⊢ a = a + (c + 1)
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.succ
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
⊢ a = a + (c + 1)
Tactic:
rcases exists_lt_omega_bodd_ne_succ a.succ with ⟨b, h0, h1⟩
Proof state after:
case intro.succ.intro.intro
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
b : ℕ
h0 : a.succ ≤ b
h1 : (Ω b).bodd ≠ (Ω b.succ).bodd
⊢ a = a + (c + 1)
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.succ.intro.intro
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
b : ℕ
h0 : a.succ ≤ b
h1 : (Ω b).bodd ≠ (Ω b.succ).bodd
⊢ a = a + (c + 1)
Tactic:
revert h1
Proof state after:
case intro.succ.intro.intro
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
b : ℕ
h0 : a.succ ≤ b
⊢ (Ω b).bodd ≠ (Ω b.succ).bodd → a = a + (c + 1)
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.succ.intro.intro
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
b : ℕ
h0 : a.succ ≤ b
⊢ (Ω b).bodd ≠ (Ω b.succ).bodd → a = a + (c + 1)
Tactic:
apply absurd
Proof state after:
case intro.succ.intro.intro.h₁
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
b : ℕ
h0 : a.succ ≤ b
⊢ (Ω b).bodd = (Ω b.succ).bodd
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.succ.intro.intro.h₁
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
b : ℕ
h0 : a.succ ≤ b
⊢ (Ω b).bodd = (Ω b.succ).bodd
Tactic:
specialize h (a * c + (b - a) * c.succ)
Proof state after:
case intro.succ.intro.intro.h₁
a c b : ℕ
h0 : a.succ ≤ b
h : Even (Ω ((a + (a * c + (b - a) * c.succ)) * (a + (c + 1) + (a * c + (b - a) * c.succ))))
⊢ (Ω b).bodd = (Ω b.succ).bodd
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.succ.intro.intro.h₁
a c b : ℕ
h0 : a.succ ≤ b
h : Even (Ω ((a + (a * c + (b - a) * c.succ)) * (a + (c + 1) + (a * c + (b - a) * c.succ))))
⊢ (Ω b).bodd = (Ω b.succ).bodd
Tactic:
rw [Even_iff_bodd, add_right_comm, ← add_assoc, a.add_comm, ← Nat.mul_succ,
  ← add_mul, Nat.add_sub_of_le (a.le_succ.trans h0), ← Nat.succ_mul] at h
Proof state after:
case intro.succ.intro.intro.h₁
a c b : ℕ
h0 : a.succ ≤ b
h : (Ω (b * c.succ * (b.succ * c.succ))).bodd = false
⊢ (Ω b).bodd = (Ω b.succ).bodd
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.succ.intro.intro.h₁
a c b : ℕ
h0 : a.succ ≤ b
h : (Ω (b * c.succ * (b.succ * c.succ))).bodd = false
⊢ (Ω b).bodd = (Ω b.succ).bodd
Tactic:
replace h0 := (Nat.zero_lt_of_lt h0).ne.symm
Proof state after:
case intro.succ.intro.intro.h₁
a c b : ℕ
h : (Ω (b * c.succ * (b.succ * c.succ))).bodd = false
h0 : b ≠ 0
⊢ (Ω b).bodd = (Ω b.succ).bodd
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.succ.intro.intro.h₁
a c b : ℕ
h : (Ω (b * c.succ * (b.succ * c.succ))).bodd = false
h0 : b ≠ 0
⊢ (Ω b).bodd = (Ω b.succ).bodd
Tactic:
have h1 := b.succ_ne_zero
Proof state after:
case intro.succ.intro.intro.h₁
a c b : ℕ
h : (Ω (b * c.succ * (b.succ * c.succ))).bodd = false
h0 : b ≠ 0
h1 : b.succ ≠ 0
⊢ (Ω b).bodd = (Ω b.succ).bodd
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.succ.intro.intro.h₁
a c b : ℕ
h : (Ω (b * c.succ * (b.succ * c.succ))).bodd = false
h0 : b ≠ 0
h1 : b.succ ≠ 0
⊢ (Ω b).bodd = (Ω b.succ).bodd
Tactic:
have h2 := c.succ_ne_zero
Proof state after:
case intro.succ.intro.intro.h₁
a c b : ℕ
h : (Ω (b * c.succ * (b.succ * c.succ))).bodd = false
h0 : b ≠ 0
h1 : b.succ ≠ 0
h2 : c.succ ≠ 0
⊢ (Ω b).bodd = (Ω b.succ).bodd
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case intro.succ.intro.intro.h₁
a c b : ℕ
h : (Ω (b * c.succ * (b.succ * c.succ))).bodd = false
h0 : b ≠ 0
h1 : b.succ ≠ 0
h2 : c.succ ≠ 0
⊢ (Ω b).bodd = (Ω b.succ).bodd
Tactic:
rwa [cardFactors_mul (Nat.mul_ne_zero h0 h2) (Nat.mul_ne_zero h1 h2),
  cardFactors_mul h0 h2, cardFactors_mul h1 h2, Nat.bodd_add,
  xor_eq_false_iff_eq, Nat.bodd_add, Nat.bodd_add, Bool.xor_right_inj] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2009N2.final_solution_part2
Proof state before:
case inr
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
this : ∀ {a b : ℕ}, (∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))) → a ≤ b → a = b
h0 : ¬a ≤ b
⊢ a = b
Tactic:
exact (this (λ k ↦ Nat.mul_comm _ _ ▸ h k) (Nat.le_of_not_ge h0)).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2017C1.sum_neg_one_pow_Ico
Proof state before:
a : ℕ
⊢ ∑ x ∈ Ico a (a + 0), (-1) ^ x = bif Nat.bodd 0 then (-1) ^ a else 0
Tactic:
rw [add_zero, Ico_self]
Proof state after:
a : ℕ
⊢ ∑ x ∈ ∅, (-1) ^ x = bif Nat.bodd 0 then (-1) ^ a else 0
Theorem: IMOSL.IMO2017C1.sum_neg_one_pow_Ico
Proof state before:
a : ℕ
⊢ ∑ x ∈ ∅, (-1) ^ x = bif Nat.bodd 0 then (-1) ^ a else 0
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2017C1.sum_neg_one_pow_Ico
Proof state before:
a : ℕ
⊢ ∑ x ∈ Ico a (a + 1), (-1) ^ x = bif Nat.bodd 1 then (-1) ^ a else 0
Tactic:
rw [Nat.Ico_succ_singleton, sum_singleton]
Proof state after:
a : ℕ
⊢ (-1) ^ a = bif Nat.bodd 1 then (-1) ^ a else 0
Theorem: IMOSL.IMO2017C1.sum_neg_one_pow_Ico
Proof state before:
a : ℕ
⊢ (-1) ^ a = bif Nat.bodd 1 then (-1) ^ a else 0
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2017C1.sum_neg_one_pow_Ico
Proof state before:
a n : ℕ
⊢ ∑ x ∈ Ico a (a + (n + 2)), (-1) ^ x = bif (n + 2).bodd then (-1) ^ a else 0
Tactic:
have h : a ≤ a + n := a.le_add_right n
Proof state after:
a n : ℕ
h : a ≤ a + n
⊢ ∑ x ∈ Ico a (a + (n + 2)), (-1) ^ x = bif (n + 2).bodd then (-1) ^ a else 0
Theorem: IMOSL.IMO2017C1.sum_neg_one_pow_Ico
Proof state before:
a n : ℕ
h : a ≤ a + n
⊢ ∑ x ∈ Ico a (a + (n + 2)), (-1) ^ x = bif (n + 2).bodd then (-1) ^ a else 0
Tactic:
rw [← add_assoc, sum_Ico_succ_top (h.trans (a + n).le_succ),
  pow_succ', neg_one_mul, sum_Ico_succ_top h, sum_neg_one_pow_Ico a n,
  add_neg_cancel_right, Nat.bodd_add, Nat.bodd_two, Bool.xor_false]
Proof state after:
no goals
Theorem: IMOSL.IMO2017C1.latticeRect_weight
Proof state before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ weight (latticeRect q) = bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
rw [weight, latticeRect, sum_product]
Proof state after:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ∑ x ∈ Ico q.1.1 (q.1.1 + q.2.1), ∑ y ∈ Ico q.1.2 (q.1.2 + q.2.2), (-1) ^ (x, y).1 * (-1) ^ (x, y).2 =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Theorem: IMOSL.IMO2017C1.latticeRect_weight
Proof state before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ∑ x ∈ Ico q.1.1 (q.1.1 + q.2.1), ∑ y ∈ Ico q.1.2 (q.1.2 + q.2.2), (-1) ^ (x, y).1 * (-1) ^ (x, y).2 =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
simp_rw [← mul_sum]
Proof state after:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ∑ x ∈ Ico q.1.1 (q.1.1 + q.2.1), (-1) ^ x * ∑ i ∈ Ico q.1.2 (q.1.2 + q.2.2), (-1) ^ i =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Theorem: IMOSL.IMO2017C1.latticeRect_weight
Proof state before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ∑ x ∈ Ico q.1.1 (q.1.1 + q.2.1), (-1) ^ x * ∑ i ∈ Ico q.1.2 (q.1.2 + q.2.2), (-1) ^ i =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
rw [← sum_mul, sum_neg_one_pow_Ico, sum_neg_one_pow_Ico]
Proof state after:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif q.2.1.bodd then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Theorem: IMOSL.IMO2017C1.latticeRect_weight
Proof state before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif q.2.1.bodd then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
cases q.2.1.bodd
Proof state after:
case false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif false then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif false && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0

case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif true && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Theorem: IMOSL.IMO2017C1.latticeRect_weight
Proof state before:
case false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif false then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif false && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0

case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif true && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
exact zero_mul _
Proof state after:
case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif true && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Theorem: IMOSL.IMO2017C1.latticeRect_weight
Proof state before:
case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif q.2.2.bodd then (-1) ^ q.1.2 else 0) =
    bif true && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
cases q.2.2.bodd
Proof state after:
case true.false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif false then (-1) ^ q.1.2 else 0) =
    bif true && false then (-1) ^ (q.1.1 + q.1.2) else 0

case true.true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif true then (-1) ^ q.1.2 else 0) =
    bif true && true then (-1) ^ (q.1.1 + q.1.2) else 0
Theorem: IMOSL.IMO2017C1.latticeRect_weight
Proof state before:
case true.false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif false then (-1) ^ q.1.2 else 0) =
    bif true && false then (-1) ^ (q.1.1 + q.1.2) else 0

case true.true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ ((bif true then (-1) ^ q.1.1 else 0) * bif true then (-1) ^ q.1.2 else 0) =
    bif true && true then (-1) ^ (q.1.1 + q.1.2) else 0
Tactic:
exacts [mul_zero _, (pow_add _ _ _).symm]
Proof state after:
no goals
Theorem: IMOSL.IMO2017C1.latticeRect_weight_pos_imp
Proof state before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ 0 < weight (latticeRect q) → (q.2.1.bodd = true ∧ q.2.2.bodd = true) ∧ (q.1.1 + q.1.2).bodd = false
Tactic:
rw [latticeRect_weight, ← Bool.and_eq_true]
Proof state after:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0) →
    (q.2.1.bodd && q.2.2.bodd) = true ∧ (q.1.1 + q.1.2).bodd = false
Theorem: IMOSL.IMO2017C1.latticeRect_weight_pos_imp
Proof state before:
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif q.2.1.bodd && q.2.2.bodd then (-1) ^ (q.1.1 + q.1.2) else 0) →
    (q.2.1.bodd && q.2.2.bodd) = true ∧ (q.1.1 + q.1.2).bodd = false
Tactic:
cases q.2.1.bodd && q.2.2.bodd
Proof state after:
case false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif false then (-1) ^ (q.1.1 + q.1.2) else 0) → false = true ∧ (q.1.1 + q.1.2).bodd = false

case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ (q.1.1 + q.1.2) else 0) → true = true ∧ (q.1.1 + q.1.2).bodd = false
Theorem: IMOSL.IMO2017C1.latticeRect_weight_pos_imp
Proof state before:
case false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif false then (-1) ^ (q.1.1 + q.1.2) else 0) → false = true ∧ (q.1.1 + q.1.2).bodd = false
Tactic:
exact λ h ↦ absurd h (le_refl 0).not_lt
Proof state after:
no goals
Theorem: IMOSL.IMO2017C1.latticeRect_weight_pos_imp
Proof state before:
case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ (q.1.1 + q.1.2) else 0) → true = true ∧ (q.1.1 + q.1.2).bodd = false
Tactic:
rw [neg_one_pow_eq_pow_mod_two (R := ℤ), Nat.mod_two_of_bodd]
Proof state after:
case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif (q.1.1 + q.1.2).bodd then 1 else 0 else 0) → true = true ∧ (q.1.1 + q.1.2).bodd = false
Theorem: IMOSL.IMO2017C1.latticeRect_weight_pos_imp
Proof state before:
case true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif (q.1.1 + q.1.2).bodd then 1 else 0 else 0) → true = true ∧ (q.1.1 + q.1.2).bodd = false
Tactic:
cases (q.1.1 + q.1.2).bodd
Proof state after:
case true.false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif false then 1 else 0 else 0) → true = true ∧ false = false

case true.true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif true then 1 else 0 else 0) → true = true ∧ true = false
Theorem: IMOSL.IMO2017C1.latticeRect_weight_pos_imp
Proof state before:
case true.false
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif false then 1 else 0 else 0) → true = true ∧ false = false

case true.true
q : (ℕ × ℕ) × ℕ × ℕ
⊢ (0 < bif true then (-1) ^ bif true then 1 else 0 else 0) → true = true ∧ true = false
Tactic:
exacts [λ _ ↦ ⟨rfl, rfl⟩, λ h ↦ absurd neg_one_lt_zero h.not_lt]
Proof state after:
no goals
Theorem: IMOSL.IMO2017C1.final_solution
Proof state before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : latticeRect ((0, 0), m, n) = I.disjiUnion (latticeRect ∘ Q) h
⊢ ∃ i ∈ I, ((Q i).2.1.bodd = true ∧ (Q i).2.2.bodd = true) ∧ ((Q i).1.1 + (Q i).1.2).bodd = false
Tactic:
suffices ∃ i ∈ I, 0 < weight (latticeRect (Q i))
  from this.elim λ i h3 ↦ ⟨i, h3.1, latticeRect_weight_pos_imp h3.2⟩
Proof state after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : latticeRect ((0, 0), m, n) = I.disjiUnion (latticeRect ∘ Q) h
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))