-- Mathlib/Order/Monotone/Basic.lean
/-- A monotone function `f : ℕ → ℕ` bounded by `b`, which is constant after stabilising for the
first time, stabilises in at most `b` steps. -/
lemma Nat.stabilises_of_monotone {f : ℕ → ℕ} {b n : ℕ} (hfmono : Monotone f) (hfb : ∀ m, f m ≤ b)
    (hfstab : ∀ m, f m = f (m + 1) → f (m + 1) = f (m + 2)) (hbn : b ≤ n) : f n = f b

Proof state:
case intro.intro
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
key : ∀ (k : ℕ), k ≥ m → f k = f m
⊢ f n = f b

Tactic:
exact (key n (hmb.trans hbn)).trans (key b hmb).symm

Result:
no goals

Proof state:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
⊢ ∃ m, m ≤ b ∧ f m = f (m + 1)

Tactic:
contrapose! hfb

Result:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
hfb : ∀ (m : ℕ), m ≤ b → f m ≠ f (m + 1)
⊢ ∃ m, b < f m

Proof state:
case intro.intro
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
key : ∀ (k : ℕ), f (m + k) = f (m + k + 1) ∧ f (m + k) = f m
⊢ f n = f b

Tactic:
replace key : ∀ k ≥ m, f k = f m := fun k hk =>
  (congr_arg f (Nat.add_sub_of_le hk)).symm.trans (key (k - m)).2

Result:
case intro.intro
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
key : ∀ (k : ℕ), k ≥ m → f k = f m
⊢ f n = f b

Proof state:
case intro.intro
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
⊢ f n = f b

Tactic:
replace key : ∀ k : ℕ, f (m + k) = f (m + k + 1) ∧ f (m + k) = f m := fun k =>
  Nat.rec ⟨hm, rfl⟩ (fun k ih => ⟨hfstab _ ih.1, ih.1.symm.trans ih.2⟩) k

Result:
case intro.intro
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
key : ∀ (k : ℕ), f (m + k) = f (m + k + 1) ∧ f (m + k) = f m
⊢ f n = f b

Proof state:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
⊢ f n = f b

Tactic:
obtain ⟨m, hmb, hm⟩ : ∃ m ≤ b, f m = f (m + 1) := by
  contrapose! hfb
  let rec strictMono : ∀ m ≤ b + 1, m ≤ f m
  | 0, _ => Nat.zero_le _
  | m + 1, hmb => (strictMono _ <| m.le_succ.trans hmb).trans_lt <| (hfmono m.le_succ).lt_of_ne <|
      hfb _ <| Nat.le_of_succ_le_succ hmb
  exact ⟨b + 1, strictMono _ le_rfl⟩

Result:
case intro.intro
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfb : ∀ (m : ℕ), f m ≤ b
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
m : ℕ
hmb : m ≤ b
hm : f m = f (m + 1)
⊢ f n = f b

Proof state:
f : ℕ → ℕ
b n : ℕ
hfmono : Monotone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
hbn : b ≤ n
hfb : ∀ (m : ℕ), m ≤ b → f m ≠ f (m + 1)
⊢ ∃ m, b < f m

Tactic:
exact ⟨b + 1, strictMono _ le_rfl⟩

Result:
no goals