-- Mathlib/Order/ScottContinuity.lean
lemma ScottContinuousOn.sup₂ {D : Set (Set (β × β))} :
    ScottContinuousOn D fun (a, b) => (a ⊔ b : β)

Proof state:
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ (fun x => x.1 ⊔ x.2) (p₁, p₂) ∈ {x | ∀ ⦃a : β⦄, a ∈ (fun x => x.1 ⊔ x.2) '' d → a ≤ x} ∧
    (fun x => x.1 ⊔ x.2) (p₁, p₂) ∈ lowerBounds {x | ∀ ⦃a : β⦄, a ∈ (fun x => x.1 ⊔ x.2) '' d → a ≤ x}

Tactic:
constructor

Result:
case left
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ (fun x => x.1 ⊔ x.2) (p₁, p₂) ∈ {x | ∀ ⦃a : β⦄, a ∈ (fun x => x.1 ⊔ x.2) '' d → a ≤ x}

case right
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ (fun x => x.1 ⊔ x.2) (p₁, p₂) ∈ lowerBounds {x | ∀ ⦃a : β⦄, a ∈ (fun x => x.1 ⊔ x.2) '' d → a ≤ x}

Proof state:
case right
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ p₁ ⊔ p₂ ∈ lowerBounds {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}

Tactic:
intro b hb

Result:
case right
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
b : β
hb : b ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
⊢ p₁ ⊔ p₂ ≤ b

Proof state:
case left
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ (fun x => x.1 ⊔ x.2) (p₁, p₂) ∈ {x | ∀ ⦃a : β⦄, a ∈ (fun x => x.1 ⊔ x.2) '' d → a ≤ x}

Tactic:
simp only [mem_image, Prod.exists, forall_exists_index, and_imp, mem_setOf_eq]

Result:
case left
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ ∀ ⦃a : β⦄ (x x_1 : β), (x, x_1) ∈ d → x ⊔ x_1 = a → a ≤ p₁ ⊔ p₂

Proof state:
case right
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ (fun x => x.1 ⊔ x.2) (p₁, p₂) ∈ lowerBounds {x | ∀ ⦃a : β⦄, a ∈ (fun x => x.1 ⊔ x.2) '' d → a ≤ x}

Tactic:
simp only [mem_image, Prod.exists, forall_exists_index, and_imp]

Result:
case right
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ p₁ ⊔ p₂ ∈ lowerBounds {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}

Proof state:
case right.a
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
b : β
hb : b ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
b₁ b₂ : β
hb' : (b₁, b₂) ∈ d
⊢ b₁ ≤ b ∧ b₂ ≤ b

Tactic:
exact sup_le_iff.mp (hb b₁ b₂ hb' rfl)

Result:
no goals

Proof state:
case left
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ a ≤ p₁ ⊔ p₂

Tactic:
rw [← hba]

Result:
case left
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ b₁ ⊔ b₂ ≤ p₁ ⊔ p₂

Proof state:
case right
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
b : β
hb : b ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x}
⊢ p₁ ≤ b ∧ p₂ ≤ b

Tactic:
rw [lowerBounds] at e1

Result:
case right
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
b : β
hb : b ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
e1 : (p₁, p₂) ∈ {x | ∀ ⦃a : β × β⦄, a ∈ {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} → x ≤ a}
⊢ p₁ ≤ b ∧ p₂ ≤ b

Proof state:
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
⊢ ScottContinuousOn D fun x => x.1 ⊔ x.2

Tactic:
intro d _ _ _ ⟨p₁, p₂⟩ hdp

Result:
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : IsLUB d (p₁, p₂)
⊢ IsLUB ((fun x => x.1 ⊔ x.2) '' d) ((fun x => x.1 ⊔ x.2) (p₁, p₂))

Proof state:
case right
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
b : β
hb : b ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
⊢ p₁ ≤ b ∧ p₂ ≤ b

Tactic:
have e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} := hdp.2

Result:
case right
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
d : Set (β × β)
a✝² : d ∈ D
a✝¹ : d.Nonempty
a✝ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
b : β
hb : b ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
e1 : (p₁, p₂) ∈ lowerBounds {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x}
⊢ p₁ ≤ b ∧ p₂ ≤ b