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