replace := le_trans le_sup_inf this
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : bᶜ ⊔ a ⊓ b ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : (bᶜ ⊔ a) ⊓ (bᶜ ⊔ b) ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c