Theorem: MinHeap.head_def (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) = ↑((head? c).untop ⋯)
Tactic:
simpa using MinHeap.coe_head_eq_head? c h
State after:
no goals