Theorem: Multiset.inf_eq_top (Algorithm/Data/Classes/MinHeap.lean)

State before:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
m : Multiset α
⊢ m.inf = ⊤ ↔ ∀ a ∈ m, a = ⊤
Tactic:
rw [le_antisymm_iff]
State after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
m : Multiset α
⊢ m.inf ≤ ⊤ ∧ ⊤ ≤ m.inf ↔ ∀ a ∈ m, a = ⊤

State before:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
m : Multiset α
⊢ m.inf ≤ ⊤ ∧ ⊤ ≤ m.inf ↔ ∀ a ∈ m, a = ⊤
Tactic:
simp
State after:
no goals