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

State before:
N : ℕ
⊢ ∃ b ∈ {n | f n < f n.succ}, N < b
Tactic:
obtain ⟨n, h0, h1⟩ : ∃ n : ℕ, N < n ∧
    ∀ k : ℕ, k < n → k.succ.divisors.card < n.succ.divisors.card := by
  obtain ⟨K, h0⟩ : ∃ K : ℕ, ∀ k : ℕ, k ≤ N → k.succ.divisors.card ≤ K :=
    ⟨Extra.seqMax (λ n ↦ n.succ.divisors.card) N,
    λ _ ↦ Extra.le_seqMax_of_le (λ n ↦ n.succ.divisors.card)⟩
  have h1 := exists_lt_card_divisor_succ K
  refine ⟨Nat.find h1,
    (Nat.lt_find_iff h1 _).mpr λ k h2 ↦ (h0 k h2).not_lt,
    λ k h2 ↦ (le_of_not_lt (Nat.find_min h1 h2)).trans_lt (Nat.find_spec h1)⟩
State after:
case intro.intro
N n : ℕ
h0 : N < n
h1 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∃ b ∈ {n | f n < f n.succ}, N < b

State before:
case intro.intro
N n : ℕ
h0 : N < n
h1 : ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
⊢ ∃ b ∈ {n | f n < f n.succ}, N < b
Tactic:
exact ⟨n, f_self_lt_f_succ_of_divisors_card (Nat.not_eq_zero_of_lt h0) h1, h0⟩
State after:
no goals

State before:
N : ℕ
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
Tactic:
obtain ⟨K, h0⟩ : ∃ K : ℕ, ∀ k : ℕ, k ≤ N → k.succ.divisors.card ≤ K :=
  ⟨Extra.seqMax (λ n ↦ n.succ.divisors.card) N,
  λ _ ↦ Extra.le_seqMax_of_le (λ n ↦ n.succ.divisors.card)⟩
State after:
case intro
N K : ℕ
h0 : ∀ k ≤ N, k.succ.divisors.card ≤ K
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card

State before:
case intro
N K : ℕ
h0 : ∀ k ≤ N, k.succ.divisors.card ≤ K
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
Tactic:
have h1 := exists_lt_card_divisor_succ K
State after:
case intro
N K : ℕ
h0 : ∀ k ≤ N, k.succ.divisors.card ≤ K
h1 : ∃ n, K < n.succ.divisors.card
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card

State before:
case intro
N K : ℕ
h0 : ∀ k ≤ N, k.succ.divisors.card ≤ K
h1 : ∃ n, K < n.succ.divisors.card
⊢ ∃ n, N < n ∧ ∀ k < n, k.succ.divisors.card < n.succ.divisors.card
Tactic:
refine ⟨Nat.find h1,
  (Nat.lt_find_iff h1 _).mpr λ k h2 ↦ (h0 k h2).not_lt,
  λ k h2 ↦ (le_of_not_lt (Nat.find_min h1 h2)).trans_lt (Nat.find_spec h1)⟩
State after:
no goals