-- Mathlib/Order/WellFoundedSet.lean
theorem PartiallyWellOrderedOn.exists_monotone_subseq (h : s.PartiallyWellOrderedOn r) (f : ℕ → α)
    (hf : ∀ n, f n ∈ s) : ∃ g : ℕ ↪o ℕ, ∀ m n : ℕ, m ≤ n → r (f (g m)) (f (g n))

Proof state:
case intro.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ False

Tactic:
obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g) fun n => hf _

Result:
case intro.inr.intro.intro.intro
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
m n : ℕ
hlt : m < n
hle : r ((f ∘ ⇑g) m) ((f ∘ ⇑g) n)
⊢ False

Proof state:
case intro.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
exfalso

Result:
case intro.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ False

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f

Result:
case intro.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

case intro.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Proof state:
case intro.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
refine ⟨g, fun m n hle => ?_⟩

Result:
case intro.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m n : ℕ
hle : m ≤ n
⊢ r (f (g m)) (f (g n))

Proof state:
case intro.inl.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m n : ℕ
hle : m ≤ n
hlt : m < n
⊢ r (f (g m)) (f (g n))

case intro.inl.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m : ℕ
hle : m ≤ m
⊢ r (f (g m)) (f (g m))

Tactic:
exacts [h1 m n hlt, refl_of r _]

Result:
no goals

Proof state:
case intro.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m n : ℕ
hle : m ≤ n
⊢ r (f (g m)) (f (g n))

Tactic:
obtain hlt | rfl := hle.lt_or_eq

Result:
case intro.inl.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m n : ℕ
hle : m ≤ n
hlt : m < n
⊢ r (f (g m)) (f (g n))

case intro.inl.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m : ℕ
hle : m ≤ m
⊢ r (f (g m)) (f (g m))

Proof state:
case intro.inr.intro.intro.intro
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
m n : ℕ
hlt : m < n
hle : r ((f ∘ ⇑g) m) ((f ∘ ⇑g) n)
⊢ False

Tactic:
exact h2 m n hlt hle

Result:
no goals