simp [inf_sup_right] at this
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ (c ⊔ bᶜ) ⊓ b
⊢ a ⊓ b ≤ c
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ c
⊢ a ⊓ b ≤ c