Theorem: MinHeap.head_mem (Algorithm/Data/Classes/MinHeap.lean)

State before:
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
h : ¬isEmpty c = true
⊢ head c h ∈ c
Tactic:
exact mem_toMultiset.mp (head_mem_toMultiset c h)
State after:
no goals