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