no goals
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ sup 0 ≤ a ↔ ∀ (b : α), b ∈ 0 → b ≤ a
simp
no goals
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (sup s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a) → (sup (a_1 ::ₘ s) ≤ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ≤ a)
simp (config := { contextual := true }) [or_imp, forall_and]