α : Type u_1
le : α → α → Bool
s : Heap α
⊢ realSize (Option.getD (tail? le s) nil) = realSize s - 1
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ realSize (tail le s) = realSize s - 1
simp only [Heap.tail]
no goals
α : Type u_1
le : α → α → Bool
s : Heap α
⊢ realSize (Option.getD (tail? le s) nil) = realSize s - 1
match eq : s.tail? le with
| none => cases s with cases eq | nil => rfl
| some tl => simp [Heap.realSize_tail? eq]; rfl
no goals
α : Type u_1
le : α → α → Bool
s : Heap α
eq : tail? le s = none
⊢ realSize (Option.getD none nil) = realSize s - 1
cases s with cases eq | nil => rfl
no goals
case nil.refl
α : Type u_1
le : α → α → Bool
⊢ realSize (Option.getD none nil) = realSize nil - 1
rfl
α : Type u_1
le : α → α → Bool
s tl : Heap α
eq : tail? le s = some tl
⊢ realSize (Option.getD (some tl) nil) = realSize tl
α : Type u_1
le : α → α → Bool
s tl : Heap α
eq : tail? le s = some tl
⊢ realSize (Option.getD (some tl) nil) = realSize s - 1
simp [Heap.realSize_tail? eq]
no goals
α : Type u_1
le : α → α → Bool
s tl : Heap α
eq : tail? le s = some tl
⊢ realSize (Option.getD (some tl) nil) = realSize tl
rfl