Theorem: MinHeap.head_le (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
x : α
hx : x ∈ c
⊢ head c ⋯ ≤ x
Tactic:
simpa [WithTop.untop_le_iff] using head?_le c x hx
State after:
no goals