no goals
ι : Type ?u.90223
α : Type u_1
β : Type ?u.90229
π : ι → Type ?u.90234
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
  codisjoint_iff]