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

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₂ : β), (b₁, b₂) ∈ d → b₁ ≤ b ∧ b₂ ≤ b

Tactic:
intro b₁ b₂ hb'

Result:
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

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 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
⊢ p₁ ≤ b ∧ p₂ ≤ b

Tactic:
apply e1

Result:
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₂ : β), (b₁, b₂) ∈ d → b₁ ≤ b ∧ b₂ ≤ 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}
a b₁ b₂ : β
hbd : (b₁, b₂) ∈ d
hba : b₁ ⊔ b₂ = a
⊢ b₁ ⊔ b₂ ≤ p₁ ⊔ p₂

Tactic:
exact sup_le_sup (hdp.1 _ _ hbd).1 (hdp.1 _ _ hbd).2

Result:
no goals

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}
⊢ IsLUB ((fun x => x.1 ⊔ x.2) '' d) ((fun x => x.1 ⊔ x.2) (p₁, p₂))

Tactic:
rw [IsLUB, IsLeast, upperBounds]

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 : (∀ (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}

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 : β⦄ (x x_1 : β), (x, x_1) ∈ d → x ⊔ x_1 = a → a ≤ p₁ ⊔ p₂

Tactic:
intro a b₁ b₂ hbd 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
⊢ a ≤ p₁ ⊔ p₂

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 : IsLUB d (p₁, p₂)
⊢ IsLUB ((fun x => x.1 ⊔ x.2) '' d) ((fun x => x.1 ⊔ x.2) (p₁, p₂))

Tactic:
rw [IsLUB, IsLeast, upperBounds] at 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 : (p₁, p₂) ∈ {x | ∀ ⦃a : β × β⦄, a ∈ d → a ≤ x} ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ ⦃a : β × β⦄, a ∈ d → a ≤ x}
⊢ 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₁ ⊔ p₂ ≤ b

Tactic:
simp only [sup_le_iff]

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₁ ≤ b ∧ p₂ ≤ b

Proof state:
β : Type u_2
inst✝ : SemilatticeSup β
D : Set (Set (β × β))
⊢ ScottContinuousOn D fun x =>
    match x with
    | (a, b) => a ⊔ b

Tactic:
simp only

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

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₂) ∈ {x | ∀ ⦃a : β × β⦄, a ∈ {x | ∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → (b₁, b₂) ≤ x} → x ≤ a}
⊢ p₁ ≤ b ∧ p₂ ≤ b

Tactic:
simp only [mem_setOf_eq, Prod.forall, Prod.mk_le_mk] 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 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
⊢ p₁ ≤ b ∧ p₂ ≤ 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 : (p₁, p₂) ∈ {x | ∀ ⦃a : β × β⦄, a ∈ d → a ≤ x} ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ ⦃a : β × β⦄, a ∈ d → a ≤ x}
⊢ IsLUB ((fun x => x.1 ⊔ x.2) '' d) ((fun x => x.1 ⊔ x.2) (p₁, p₂))

Tactic:
simp only [Prod.forall, mem_setOf_eq, Prod.mk_le_mk] at 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 : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
⊢ IsLUB ((fun x => x.1 ⊔ x.2) '' d) ((fun x => x.1 ⊔ x.2) (p₁, p₂))