Theorem: IMOSL.IMO2006N3.final_solution_part2 (IMOSLLean4/IMO2006/N3/N3.lean)

State before:
N : ℕ
⊢ ∃ b ∈ {n | f n.succ < f n}, N < b
Tactic:
obtain ⟨n, h, h0, h1⟩ : ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n := by
  rcases (max 6 (N + 1) + 1).exists_infinite_primes with ⟨_ | n, h, h0⟩
  exact absurd h0 Nat.not_prime_zero
  rw [Nat.add_le_add_iff_right, max_le_iff] at h
  exact ⟨n, h.1, h0, h.2⟩
State after:
case intro.intro.intro
N n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
h1 : N < n
⊢ ∃ b ∈ {n | f n.succ < f n}, N < b

State before:
case intro.intro.intro
N n : ℕ
h : 6 ≤ n
h0 : n.succ.Prime
h1 : N < n
⊢ ∃ b ∈ {n | f n.succ < f n}, N < b
Tactic:
exact ⟨n, f_succ_lt_self_of_succ_prime_large h h0, h1⟩
State after:
no goals

State before:
N : ℕ
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Tactic:
rcases (max 6 (N + 1) + 1).exists_infinite_primes with ⟨_ | n, h, h0⟩
State after:
case intro.zero.intro
N : ℕ
h : max 6 (N + 1) + 1 ≤ 0
h0 : Nat.Prime 0
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n

case intro.succ.intro
N n : ℕ
h : max 6 (N + 1) + 1 ≤ n + 1
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n

State before:
case intro.zero.intro
N : ℕ
h : max 6 (N + 1) + 1 ≤ 0
h0 : Nat.Prime 0
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n

case intro.succ.intro
N n : ℕ
h : max 6 (N + 1) + 1 ≤ n + 1
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Tactic:
exact absurd h0 Nat.not_prime_zero
State after:
case intro.succ.intro
N n : ℕ
h : max 6 (N + 1) + 1 ≤ n + 1
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n

State before:
case intro.succ.intro
N n : ℕ
h : max 6 (N + 1) + 1 ≤ n + 1
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Tactic:
rw [Nat.add_le_add_iff_right, max_le_iff] at h
State after:
case intro.succ.intro
N n : ℕ
h : 6 ≤ n ∧ N + 1 ≤ n
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n

State before:
case intro.succ.intro
N n : ℕ
h : 6 ≤ n ∧ N + 1 ≤ n
h0 : (n + 1).Prime
⊢ ∃ n, 6 ≤ n ∧ n.succ.Prime ∧ N < n
Tactic:
exact ⟨n, h.1, h0, h.2⟩
State after:
no goals