-- Mathlib/Order/ScottContinuity.lean
lemma ScottContinuousOn.prodMk (hD : ∀ a b : α, a ≤ b → {a, b} ∈ D)
    (hf : ScottContinuousOn D f) (hg : ScottContinuousOn D g) :
    ScottContinuousOn D fun x => (f x, g x) := fun d hd₁ hd₂ hd₃ a hda => by
  rw [IsLUB, IsLeast, upperBounds]
  constructor
  · simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq,
      Prod.mk_le_mk]
    intro b hb
    exact ⟨hf.monotone D hD (hda.1 hb), hg.monotone D hD (hda.1 hb)⟩
  · intro ⟨p₁, p₂⟩ hp
    simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq,
      Prod.mk_le_mk] at hp
    constructor
    · rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
      intro _ hb
      exact (hp _ hb).1
    · rw [isLUB_le_iff (hg hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
      intro _ hb
      exact (hp _ hb).2

Proof state:
case right.right
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).2 ∈ {x | ∀ ⦃a : β⦄, a ∈ g '' d → a ≤ x}

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]

Result:
case right.right
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ∀ a ∈ d, g a ≤ p₂

Proof state:
case right.left
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x => (f x, g x)) a).1 ≤ (p₁, p₂).1

Tactic:
rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds]

Result:
case right.left
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).1 ∈ {x | ∀ ⦃a : β⦄, a ∈ f '' d → a ≤ x}

Proof state:
case left
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ (fun x => (f x, g x)) a ∈ {x | ∀ ⦃a : β × β⦄, a ∈ (fun x => (f x, g x)) '' d → a ≤ x}

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq,
  Prod.mk_le_mk]

Result:
case left
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ ∀ a_1 ∈ d, f a_1 ≤ f a ∧ g a_1 ≤ g a

Proof state:
case right
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (fun x => (f x, g x)) a ≤ (p₁, p₂)

Tactic:
constructor

Result:
case right.left
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x => (f x, g x)) a).1 ≤ (p₁, p₂).1

case right.right
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x => (f x, g x)) a).2 ≤ (p₁, p₂).2

Proof state:
case right
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : (p₁, p₂) ∈ {x | ∀ ⦃a : β × β⦄, a ∈ (fun x => (f x, g x)) '' d → a ≤ x}
⊢ (fun x => (f x, g x)) a ≤ (p₁, p₂)

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq,
  Prod.mk_le_mk] at hp

Result:
case right
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (fun x => (f x, g x)) a ≤ (p₁, p₂)

Proof state:
case left
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
b : α
hb : b ∈ d
⊢ f b ≤ f a ∧ g b ≤ g a

Tactic:
exact ⟨hf.monotone D hD (hda.1 hb), hg.monotone D hD (hda.1 hb)⟩

Result:
no goals

Proof state:
case right.left
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
a✝ : α
hb : a✝ ∈ d
⊢ f a✝ ≤ p₁

Tactic:
exact (hp _ hb).1

Result:
no goals

Proof state:
case right.left
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).1 ∈ {x | ∀ ⦃a : β⦄, a ∈ f '' d → a ≤ x}

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]

Result:
case right.left
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
f g : α → β
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ p₂ : β
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ∀ a ∈ d, f a ≤ p₁