ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
⊢ PartiallyWellOrderedOn (s ∪ t) r
rintro f hf
case intro.inl
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (↑g n) ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

case intro.inr
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (↑g n) ∈ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)
rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hgs | hgt⟩
case intro.inl.intro.intro.intro
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (↑g n) ∈ s
m n : ℕ
hlt : m < n
hr : r (f (↑g m)) (f (↑g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)
case intro.inl
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (↑g n) ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)
rcases hs _ hgs with ⟨m, n, hlt, hr⟩
no goals
case intro.inl.intro.intro.intro
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), f (↑g n) ∈ s
m n : ℕ
hlt : m < n
hr : r (f (↑g m)) (f (↑g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)
exact ⟨g m, g n, g.strictMono hlt, hr⟩
case intro.inr.intro.intro.intro
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (↑g n) ∈ t
m n : ℕ
hlt : m < n
hr : r (f (↑g m)) (f (↑g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)
case intro.inr
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (↑g n) ∈ t
⊢ ∃ m n, m < n ∧ r (f m) (f n)
rcases ht _ hgt with ⟨m, n, hlt, hr⟩
no goals
case intro.inr.intro.intro.intro
ι : Type ?u.44198
α : Type u_1
β : Type ?u.44204
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t : Set α
a : α
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), f (↑g n) ∈ t
m n : ℕ
hlt : m < n
hr : r (f (↑g m)) (f (↑g n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)
exact ⟨g m, g n, g.strictMono hlt, hr⟩