case intro.inl
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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))
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (↑g m)) (f (↑g n))
obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq r f
case intro.inl
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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))
case intro.inl
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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))
refine' ⟨g, fun m n hle => _⟩
case intro.inl.inl
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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))
case intro.inl
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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))
obtain hlt | rfl := hle.lt_or_eq
no goals
case intro.inl.inl
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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))
exacts [h1 m n hlt, refl_of r _]
case intro.inr.h
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
⊢ False
case intro.inr
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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))
exfalso
case intro.inr.h.intro.intro.intro
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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
case intro.inr.h
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬r (f (↑g m)) (f (↑g n))
⊢ False
obtain ⟨m, n, hlt, hle⟩ := h (f ∘ g) fun n => hf _
no goals
case intro.inr.h.intro.intro.intro
ι : Type ?u.83266
α : Type u_1
β : Type ?u.83272
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
h : PartiallyWellOrderedOn s 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
exact h2 m n hlt hle