no goals
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
rw [inf_sup_right, ← inf_assoc, h.inf_eq_bot, bot_inf_eq, bot_sup_eq, inf_left_comm,
h'.inf_eq_bot, inf_bot_eq]
no goals
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y z x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
rw [sup_inf_left, @sup_comm _ _ x, sup_assoc, h.sup_eq_top, sup_top_eq, top_inf_eq,
sup_assoc, sup_left_comm, h'.sup_eq_top, sup_top_eq]