Theorem: IMOSL.IMO2009N2.final_solution_part1 (IMOSLLean4/IMO2009/N2/N2.lean)

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
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)))

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
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)))

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
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)))

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
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)))

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⟩
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)))

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 ↦ ?_⟩
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)))

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
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)))

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]
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

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⟩
State after:
no goals