Theorem: MinHeap.eq_head_of_forall_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
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ∀ y ∈ c, p y → y ≠ x → x < y
⊢ x = head c hc
Tactic:
apply WithTop.coe_injective
State after:
case a
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ∀ y ∈ c, p y → y ≠ x → x < y
⊢ ↑x = ↑(head c hc)

State before:
case a
C : Type u_1
α : Type u_2
inst✝² : Preorder α
inst✝¹ : IsTotalPreorder α fun x x_1 => x ≤ x_1
inst✝ : MinHeap C α
c : C
p : α → Prop
hc : ¬isEmpty c = true
pc : p (head c hc)
x : α
hx : x ∈ c
h : ∀ y ∈ c, p y → y ≠ x → x < y
⊢ ↑x = ↑(head c hc)
Tactic:
simpa using coe_eq_head?_of_forall_le c p hc pc x hx h
State after:
no goals