no goals
α : Type u_1
ι : Sort ?u.9874
κ : ι → Sort ?u.9879
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ ↑c.toOrderHom (↑c.toOrderHom x ⊔ ↑c.toOrderHom y) = ↑c.toOrderHom (x ⊔ y)
rw [closure_sup_closure_left, closure_sup_closure_right]