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

State before:
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
⊢ a = b
Tactic:
wlog h0 : a ≤ b
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

State before:
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
h0 : a ≤ b
⊢ a = b
Tactic:
rw [le_iff_exists_add] at h0
State after:
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
h0 : ∃ c, b = a + c
⊢ a = b

State before:
a b : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (b + k)))
h0 : ∃ c, b = a + c
⊢ a = b
Tactic:
rcases h0 with ⟨_ | c, rfl⟩
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)

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
State after:
case intro.succ
a c : ℕ
h : ∀ (k : ℕ), Even (Ω ((a + k) * (a + (c + 1) + k)))
⊢ a = a + (c + 1)

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

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

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

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

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

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

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

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

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

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