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

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ↔ a ⊓ bᶜ ≤ ⊥
Tactic:
conv => lhs; rhs; rw [← compl_compl b]
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:
have : bᶜᶜ = bᶜᶜ ⊔ ⊥ := by exact (sup_bot_eq _).symm
State after:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
this : bᶜᶜ = bᶜᶜ ⊔ ⊥
⊢ a ≤ bᶜᶜ ↔ a ⊓ bᶜ ≤ ⊥

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

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

State before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ bᶜᶜ = bᶜᶜ ⊔ ⊥
Tactic:
exact (sup_bot_eq _).symm
State after:
no goals