F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
key : ∃ n, n ≤ B ∧ f n = f (n + 1)
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
have key : ∃ n : ℕ, n ≤ B ∧ f n = f (n + 1) := by
  contrapose! h2
  suffices ∀ n : ℕ, n ≤ B + 1 → n ≤ f n by exact ⟨B + 1, this (B + 1) (le_refl (B + 1))⟩
  exact fun n =>
    Nat.rec (fun _ => Nat.zero_le (f 0))
      (fun n ih h =>
        lt_of_le_of_lt (ih (n.le_succ.trans h))
          (lt_of_le_of_ne (h1 n.le_succ) (h2 n (Nat.succ_le_succ_iff.mp h))))
      n
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
h2 : ∀ (n : ℕ), n ≤ B → f n ≠ f (n + 1)
⊢ ∃ n, B < f n
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
⊢ ∃ n, n ≤ B ∧ f n = f (n + 1)
contrapose! h2
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
h2 : ∀ (n : ℕ), n ≤ B → f n ≠ f (n + 1)
⊢ ∀ (n : ℕ), n ≤ B + 1 → n ≤ f n
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
h2 : ∀ (n : ℕ), n ≤ B → f n ≠ f (n + 1)
⊢ ∃ n, B < f n
suffices ∀ n : ℕ, n ≤ B + 1 → n ≤ f n by exact ⟨B + 1, this (B + 1) (le_refl (B + 1))⟩
no goals
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
h2 : ∀ (n : ℕ), n ≤ B → f n ≠ f (n + 1)
⊢ ∀ (n : ℕ), n ≤ B + 1 → n ≤ f n
exact fun n =>
  Nat.rec (fun _ => Nat.zero_le (f 0))
    (fun n ih h =>
      lt_of_le_of_lt (ih (n.le_succ.trans h))
        (lt_of_le_of_ne (h1 n.le_succ) (h2 n (Nat.succ_le_succ_iff.mp h))))
    n
no goals
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
h2 : ∀ (n : ℕ), n ≤ B → f n ≠ f (n + 1)
this : ∀ (n : ℕ), n ≤ B + 1 → n ≤ f n
⊢ ∃ n, B < f n
exact ⟨B + 1, this (B + 1) (le_refl (B + 1))⟩
case intro.intro
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
n : ℕ
hn1 : n ≤ B
hn2 : f n = f (n + 1)
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
key : ∃ n, n ≤ B ∧ f n = f (n + 1)
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
obtain ⟨n, hn1, hn2⟩ := key
case intro.intro
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
n : ℕ
hn1 : n ≤ B
hn2 : f n = f (n + 1)
key : ∀ (k : ℕ), f (n + k) = f (n + k + 1) ∧ f (n + k) = f n
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
case intro.intro
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
n : ℕ
hn1 : n ≤ B
hn2 : f n = f (n + 1)
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
replace key : ∀ k : ℕ, f (n + k) = f (n + k + 1) ∧ f (n + k) = f n := fun k =>
  Nat.rec ⟨hn2, rfl⟩ (fun k ih => ⟨h3 _ ih.1, ih.1.symm.trans ih.2⟩) k
case intro.intro
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
n : ℕ
hn1 : n ≤ B
hn2 : f n = f (n + 1)
key : ∀ (k : ℕ), n ≤ k → f k = f n
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
case intro.intro
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
n : ℕ
hn1 : n ≤ B
hn2 : f n = f (n + 1)
key : ∀ (k : ℕ), f (n + k) = f (n + k + 1) ∧ f (n + k) = f n
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
replace key : ∀ k : ℕ, n ≤ k → f k = f n := fun k hk =>
  (congr_arg f (add_tsub_cancel_of_le hk)).symm.trans (key (k - n)).2
no goals
case intro.intro
F : Type ?u.162814
α : Type ?u.162817
β : Type ?u.162820
γ : Type ?u.162823
f : ℕ → ℕ
h1 : Monotone f
B : ℕ
h2 : ∀ (n : ℕ), f n ≤ B
h3 : ∀ (n : ℕ), f n = f (n + 1) → f (n + 1) = f (n + 2)
n : ℕ
hn1 : n ≤ B
hn2 : f n = f (n + 1)
key : ∀ (k : ℕ), n ≤ k → f k = f n
⊢ ∀ (k : ℕ), B ≤ k → f k = f B
exact fun k hk => (key k (hn1.trans hk)).trans (key B hn1).symm