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

State before:
a : ℕ
⊢ ∃ b, a ≤ b ∧ (Ω b).bodd ≠ (Ω b.succ).bodd
Tactic:
by_contra h
State after:
a : ℕ
h : ¬∃ b, a ≤ b ∧ (Ω b).bodd ≠ (Ω b.succ).bodd
⊢ False

State before:
a : ℕ
h : ¬∃ b, a ≤ b ∧ (Ω b).bodd ≠ (Ω b.succ).bodd
⊢ False
Tactic:
rw [not_exists] at h
State after:
a : ℕ
h : ∀ (x : ℕ), ¬(a ≤ x ∧ (Ω x).bodd ≠ (Ω x.succ).bodd)
⊢ False

State before:
a : ℕ
h : ∀ (x : ℕ), ¬(a ≤ x ∧ (Ω x).bodd ≠ (Ω x.succ).bodd)
⊢ False
Tactic:
simp_rw [not_and, not_not] at h
State after:
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
⊢ False

State before:
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
⊢ False
Tactic:
rcases a.exists_infinite_primes with ⟨p, h0, h1⟩
State after:
case intro.intro
a : ℕ
h : ∀ (x : ℕ), a ≤ x → (Ω x).bodd = (Ω x.succ).bodd
p : ℕ
h0 : a ≤ p
h1 : p.Prime
⊢ False

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

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

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