Sup vs sup

Stream: general

[Johan Commelin]

Is there something in mathlib expressing compatibility between Sup and sup for complete lattices?
I would expect something like

lemma Sup_eq_sup (a b : X) : Sup {x | x = a \or x = b} = a \sqcup b := sorry

[Mario Carneiro]

that's Sup {a, b} on the left, did you look for that?

[Mario Carneiro]

also it might be expressed in terms of Sup (insert a s)

[Johan Commelin]

Aah, there is a Sup_insert. And that can be chained with Sup_singleton