ι : Type ?u.91578
α : Type u_2
β : Type u_1
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
⊢ ∃ m n, m < n ∧ (fun x y => r x.fst y.fst ∧ r' x.snd y.snd) (f m) (f n)
ι : Type ?u.91578
α : Type u_2
β : Type u_1
r : α → α → Prop
r' : β → β → Prop
f : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
⊢ PartiallyWellOrderedOn (s ×ˢ t) fun x y => r x.fst y.fst ∧ r' x.snd y.snd
intro f hf
case intro
ι : Type ?u.91578
α : Type u_2
β : Type u_1
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (↑g₁ m)) ((Prod.fst ∘ f) (↑g₁ n))
⊢ ∃ m n, m < n ∧ (fun x y => r x.fst y.fst ∧ r' x.snd y.snd) (f m) (f n)
ι : Type ?u.91578
α : Type u_2
β : Type u_1
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
⊢ ∃ m n, m < n ∧ (fun x y => r x.fst y.fst ∧ r' x.snd y.snd) (f m) (f n)
obtain ⟨g₁, h₁⟩ := hs.exists_monotone_subseq (Prod.fst ∘ f) fun n => (hf n).1
case intro.intro.intro.intro
ι : Type ?u.91578
α : Type u_2
β : Type u_1
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (↑g₁ m)) ((Prod.fst ∘ f) (↑g₁ n))
m n : ℕ
hlt : m < n
hle : r' ((Prod.snd ∘ f ∘ ↑g₁) m) ((Prod.snd ∘ f ∘ ↑g₁) n)
⊢ ∃ m n, m < n ∧ (fun x y => r x.fst y.fst ∧ r' x.snd y.snd) (f m) (f n)
case intro
ι : Type ?u.91578
α : Type u_2
β : Type u_1
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (↑g₁ m)) ((Prod.fst ∘ f) (↑g₁ n))
⊢ ∃ m n, m < n ∧ (fun x y => r x.fst y.fst ∧ r' x.snd y.snd) (f m) (f n)
obtain ⟨m, n, hlt, hle⟩ := ht (Prod.snd ∘ f ∘ g₁) fun n => (hf _).2
no goals
case intro.intro.intro.intro
ι : Type ?u.91578
α : Type u_2
β : Type u_1
r : α → α → Prop
r' : β → β → Prop
f✝ : α → β
s t✝ : Set α
a : α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : PartiallyWellOrderedOn s r
ht : PartiallyWellOrderedOn t r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (↑g₁ m)) ((Prod.fst ∘ f) (↑g₁ n))
m n : ℕ
hlt : m < n
hle : r' ((Prod.snd ∘ f ∘ ↑g₁) m) ((Prod.snd ∘ f ∘ ↑g₁) n)
⊢ ∃ m n, m < n ∧ (fun x y => r x.fst y.fst ∧ r' x.snd y.snd) (f m) (f n)
exact ⟨g₁ m, g₁ n, g₁.strictMono hlt, h₁ _ _ hlt.le, hle⟩