α : Type u_1
s✝ : Heap α
le : α → α → Bool
k : Heap α → Heap α
res : FindMin α
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ (findMin le (k ∘ cons r a c) s
        (if le res.val a = true then res else { before := k, val := a, node := c, next := s })).val =
    headD le (if le res.val a = true then res.val else a) s
α : Type u_1
s✝ : Heap α
le : α → α → Bool
k : Heap α → Heap α
res : FindMin α
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ (findMin le k (cons r a c s) res).val = headD le res.val (cons r a c s)
rw [findMin, headD]
no goals
α : Type u_1
s✝ : Heap α
le : α → α → Bool
k : Heap α → Heap α
res : FindMin α
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ (findMin le (k ∘ cons r a c) s
        (if le res.val a = true then res else { before := k, val := a, node := c, next := s })).val =
    headD le (if le res.val a = true then res.val else a) s
split <;> apply findMin_val