no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t : Set α
a✝ b a : α
s : Set α
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s
rw [insert_eq, upperBounds_union, upperBounds_singleton]