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

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ↔ a ⊓ bᶜ = ⊥
Tactic:
rw [← le_bot_iff]
State after:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ↔ a ⊓ bᶜ ≤ ⊥

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