α : Type u_1
le : α → α → Bool
n : Nat
k : Heap α → Heap α
res : FindMin α
s✝ : Heap α
hr : FindMin.WellFormed le res
hk : ∀ {s : Heap α}, WellFormed le n s → WellFormed le 0 (k s)
r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
h₁ : n ≤ r
h₂ : HeapNode.WellFormed le a c r
h₃ : WellFormed le (r + 1) s
⊢ Nonempty (FindMin.WellFormed le (Heap.findMin le k (cons r a c s) res))
α : Type u_1
le : α → α → Bool
n : Nat
k : Heap α → Heap α
res : FindMin α
s✝ : Heap α
hr : FindMin.WellFormed le res
hk : ∀ {s : Heap α}, WellFormed le n s → WellFormed le 0 (k s)
r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
⊢ Nonempty (FindMin.WellFormed le (Heap.findMin le k (cons r a c s) res))
let ⟨h₁, h₂, h₃⟩ := h
α : Type u_1
le : α → α → Bool
n : Nat
k : Heap α → Heap α
res : FindMin α
s✝ : Heap α
hr : FindMin.WellFormed le res
hk : ∀ {s : Heap α}, WellFormed le n s → WellFormed le 0 (k s)
r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
h₁ : n ≤ r
h₂ : HeapNode.WellFormed le a c r
h₃ : WellFormed le (r + 1) s
⊢ Nonempty
    (FindMin.WellFormed le
      (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 })))
α : Type u_1
le : α → α → Bool
n : Nat
k : Heap α → Heap α
res : FindMin α
s✝ : Heap α
hr : FindMin.WellFormed le res
hk : ∀ {s : Heap α}, WellFormed le n s → WellFormed le 0 (k s)
r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
h₁ : n ≤ r
h₂ : HeapNode.WellFormed le a c r
h₃ : WellFormed le (r + 1) s
⊢ Nonempty (FindMin.WellFormed le (Heap.findMin le k (cons r a c s) res))
simp [Heap.findMin]
case inl
α : Type u_1
le : α → α → Bool
n : Nat
k : Heap α → Heap α
res : FindMin α
s✝ : Heap α
hr : FindMin.WellFormed le res
hk : ∀ {s : Heap α}, WellFormed le n s → WellFormed le 0 (k s)
r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
h₁ : n ≤ r
h₂ : HeapNode.WellFormed le a c r
h₃ : WellFormed le (r + 1) s
h✝ : le res.val a = true
⊢ Nonempty (FindMin.WellFormed le (Heap.findMin le (k ∘ cons r a c) s res))

case inr
α : Type u_1
le : α → α → Bool
n : Nat
k : Heap α → Heap α
res : FindMin α
s✝ : Heap α
hr : FindMin.WellFormed le res
hk : ∀ {s : Heap α}, WellFormed le n s → WellFormed le 0 (k s)
r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
h₁ : n ≤ r
h₂ : HeapNode.WellFormed le a c r
h₃ : WellFormed le (r + 1) s
h✝ : ¬le res.val a = true
⊢ Nonempty (FindMin.WellFormed le (Heap.findMin le (k ∘ cons r a c) s { before := k, val := a, node := c, next := s }))
α : Type u_1
le : α → α → Bool
n : Nat
k : Heap α → Heap α
res : FindMin α
s✝ : Heap α
hr : FindMin.WellFormed le res
hk : ∀ {s : Heap α}, WellFormed le n s → WellFormed le 0 (k s)
r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
h₁ : n ≤ r
h₂ : HeapNode.WellFormed le a c r
h₃ : WellFormed le (r + 1) s
⊢ Nonempty
    (FindMin.WellFormed le
      (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 })))
split
no goals
case inl
α : Type u_1
le : α → α → Bool
n : Nat
k : Heap α → Heap α
res : FindMin α
s✝ : Heap α
hr : FindMin.WellFormed le res
hk : ∀ {s : Heap α}, WellFormed le n s → WellFormed le 0 (k s)
r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
h₁ : n ≤ r
h₂ : HeapNode.WellFormed le a c r
h₃ : WellFormed le (r + 1) s
h✝ : le res.val a = true
⊢ Nonempty (FindMin.WellFormed le (Heap.findMin le (k ∘ cons r a c) s res))
exact findMin h₃ hr (fun h => hk ⟨h₁, h₂, h⟩)
no goals
case inr
α : Type u_1
le : α → α → Bool
n : Nat
k : Heap α → Heap α
res : FindMin α
s✝ : Heap α
hr : FindMin.WellFormed le res
hk : ∀ {s : Heap α}, WellFormed le n s → WellFormed le 0 (k s)
r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
h₁ : n ≤ r
h₂ : HeapNode.WellFormed le a c r
h₃ : WellFormed le (r + 1) s
h✝ : ¬le res.val a = true
⊢ Nonempty (FindMin.WellFormed le (Heap.findMin le (k ∘ cons r a c) s { before := k, val := a, node := c, next := s }))
exact findMin h₃ ⟨_, fun h => hk (h.of_le h₁), h₂, h₃⟩ (fun h => hk ⟨h₁, h₂, h⟩)