Theorem: MinHeap.head?_ne_top (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 ≠ ⊤
Tactic:
intro hc
State after:
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
hc : head? c = ⊤
⊢ False

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
hc : head? c = ⊤
⊢ False
Tactic:
have := hc ▸ (head?_mem_toMultiset_map c h)
State after:
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
hc : head? c = ⊤
this : ⊤ ∈ Multiset.map WithTop.some (toMultiset c)
⊢ False

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
hc : head? c = ⊤
this : ⊤ ∈ Multiset.map WithTop.some (toMultiset c)
⊢ False
Tactic:
simp at this
State after:
no goals