case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ p.fst ≤ a

case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ p.snd ≤ a

case refine'_3
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
⊢ p ∈ upperBounds s

case refine'_4
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
⊢ p ∈ lowerBounds (upperBounds s)
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
refine'
  ⟨fun H =>
    ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => _⟩,
      ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => _⟩⟩,
    fun H => ⟨_, _⟩⟩
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ (a, p.snd) ∈ upperBounds s
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ p.fst ≤ a
suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
no goals
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ (a, p.snd) ∈ upperBounds s
exact fun q hq => ⟨ha <| mem_image_of_mem _ hq, (H.1 hq).2⟩
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ (p.fst, a) ∈ upperBounds s
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ p.snd ≤ a
suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
no goals
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ (p.fst, a) ∈ upperBounds s
exact fun q hq => ⟨(H.1 hq).1, ha <| mem_image_of_mem _ hq⟩
no goals
case refine'_3
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
⊢ p ∈ upperBounds s
exact fun q hq => ⟨H.1.1 <| mem_image_of_mem _ hq, H.2.1 <| mem_image_of_mem _ hq⟩
no goals
case refine'_4
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB (Prod.fst '' s) p.fst ∧ IsLUB (Prod.snd '' s) p.snd
⊢ p ∈ lowerBounds (upperBounds s)
exact fun q hq =>
  ⟨H.1.2 <| monotone_fst.mem_upperBounds_image hq,
    H.2.2 <| monotone_snd.mem_upperBounds_image hq⟩