Theorem: MinHeap.head_mem_toMultiset (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 ∈ toMultiset c
Tactic:
obtain ⟨x, hx₁, hx₂⟩ := Multiset.mem_map.mp (head?_mem_toMultiset_map c h)
State after:
case intro.intro
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
x : α
hx₁ : x ∈ toMultiset c
hx₂ : ↑x = head? c
⊢ head c h ∈ toMultiset c

State before:
case intro.intro
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
x : α
hx₁ : x ∈ toMultiset c
hx₂ : ↑x = head? c
⊢ head c h ∈ toMultiset c
Tactic:
simp [hx₁, ← hx₂]
State after:
no goals