α : Type u
β : Type v
γ : Type ?u.26825
δ : Type ?u.26828
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
α : Type u
β : Type v
γ : Type ?u.26825
δ : Type ?u.26828
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
rw [eq_bot_iff, sup_le_iff]
no goals
α : Type u
β : Type v
γ : Type ?u.26825
δ : Type ?u.26828
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
simp