-- Mathlib/Order/OrderIsoNat.lean
theorem exists_increasing_or_nonincreasing_subseq (r : α → α → Prop) [IsTrans α r] (f : ℕ → α) :
    ∃ g : ℕ ↪o ℕ,
      (∀ m n : ℕ, m < n → r (f (g m)) (f (g n))) ∨ ∀ m n : ℕ, m < n → ¬r (f (g m)) (f (g n))

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
ih : m < m.succ + x → r (f (g m)) (f (g (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f (g m)) (f (g (m.succ.add x)))

Tactic:
exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f

Result:
case intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

case intro.inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Proof state:
case intro.inl.intro.zero
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m : ℕ
mn : m < m.succ + 0
⊢ r (f (g m)) (f (g (m.succ + 0)))

Tactic:
apply hr

Result:
no goals

Proof state:
case intro.inr
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
exact ⟨g, Or.intro_right _ hnr⟩

Result:
no goals

Proof state:
case intro.inl.intro.succ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
ih : m < m.succ + x → r (f (g m)) (f (g (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f (g m)) (f (g (m.succ + (x + 1))))

Tactic:
apply IsTrans.trans _ _ _ _ (hr _)

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
ih : m < m.succ + x → r (f (g m)) (f (g (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f (g m)) (f (g (m.succ.add x)))

Proof state:
case intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
⊢ ∃ g, (∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩

Result:
case intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m n : ℕ
mn : m < n
⊢ r (f (g m)) (f (g n))

Proof state:
case intro.inl.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
mn : m < m.succ + x
⊢ r (f (g m)) (f (g (m.succ + x)))

Tactic:
induction' x with x ih

Result:
case intro.inl.intro.zero
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m : ℕ
mn : m < m.succ + 0
⊢ r (f (g m)) (f (g (m.succ + 0)))

case intro.inl.intro.succ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
ih : m < m.succ + x → r (f (g m)) (f (g (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f (g m)) (f (g (m.succ + (x + 1))))

Proof state:
case intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m n : ℕ
mn : m < n
⊢ r (f (g m)) (f (g n))

Tactic:
obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)

Result:
case intro.inl.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))
m x : ℕ
mn : m < m.succ + x
⊢ r (f (g m)) (f (g (m.succ + x)))