Theorem: BooleanAlgebra.inf_compl_le_iff_le_sup (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ bᶜ ≤ c ↔ a ≤ b ⊔ c
Tactic:
conv => rhs; rhs; lhs; rw [← compl_compl b]
State after:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ bᶜ ≤ c ↔ a ≤ bᶜᶜ ⊔ c

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ bᶜ ≤ c ↔ a ≤ bᶜᶜ ⊔ c
Tactic:
exact BooleanAlgebra.inf_le_iff_le_compl_sup
State after:
no goals