have : a ⊓ b ≤ (c ⊔ bᶜ) ⊓ b := inf_le_inf_right b h
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
⊢ a ⊓ b ≤ c
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ (c ⊔ bᶜ) ⊓ b
⊢ a ⊓ b ≤ c