simp only [compl_sup_eq_top, ge_iff_le, le_top, inf_of_le_left, sup_le_iff, le_sup_left,
  true_and] at this
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : (bᶜ ⊔ a) ⊓ (bᶜ ⊔ b) ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : a ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c