no goals
α : Type u_1
ι : Sort ?u.30384
κ : ι → Sort ?u.30389
β : Type u_2
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
x y : α
⊢ toFun l (↑(toFun l ↑x) ∪ ↑(toFun l ↑y)) = toFun l (↑x ∪ ↑y)
rw [closure_union_closure_right, closure_union_closure_left]