α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
⊢ Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl → WF le tl
α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
⊢ Heap.tail? le s = some tl → WF le tl
simp only [Heap.tail?]
α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl
⊢ WF le tl
α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
⊢ Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl → WF le tl
intro eq
no goals
α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl
⊢ WF le tl
match eq₂ : s.deleteMin le, eq with
| some (a, tl), rfl => exact hwf.deleteMin eq₂
no goals
α : Type u_1
s : Heap α
le : α → α → Bool
tl✝ : Heap α
hwf : WF le s
eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl✝
a : α
tl : Heap α
eq₂ : Heap.deleteMin le s = some (a, tl)
⊢ WF le ((fun x => x.snd) (a, tl))
exact hwf.deleteMin eq₂