case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
⊢ WellFormed le 0
    (Heap.merge le
      (HeapNode.toHeap (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node)
      (FindMin.before (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })
        (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))
α : Type u_1
le : α → α → Bool
n : Nat
a : α
s' s : Heap α
h : WellFormed le n s
eq : Heap.deleteMin le s = some (a, s')
⊢ WellFormed le 0 s'
cases s with cases eq | cons r a c s => ?_
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
this :
  Nonempty (FindMin.WellFormed le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }))
⊢ WellFormed le 0
    (Heap.merge le
      (HeapNode.toHeap (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node)
      (FindMin.before (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })
        (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
⊢ WellFormed le 0
    (Heap.merge le
      (HeapNode.toHeap (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node)
      (FindMin.before (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })
        (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))
have : Nonempty ((s.findMin le (cons r a c) ⟨id, a, c, s⟩).WellFormed le) :=
  let ⟨_, h₂, h₃⟩ := h
  h₃.findMin ⟨_, fun h => h.of_le (Nat.zero_le _), h₂, h₃⟩
    fun h => ⟨Nat.zero_le _, h₂, h⟩
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
⊢ Nonempty (FindMin.WellFormed le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })) →
    WellFormed le 0
      (Heap.merge le
        (HeapNode.toHeap (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node)
        (FindMin.before (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })
          (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
this :
  Nonempty (FindMin.WellFormed le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }))
⊢ WellFormed le 0
    (Heap.merge le
      (HeapNode.toHeap (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node)
      (FindMin.before (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })
        (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))
revert this
no goals
case cons.refl
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
⊢ Nonempty (FindMin.WellFormed le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })) →
    WellFormed le 0
      (Heap.merge le
        (HeapNode.toHeap (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node)
        (FindMin.before (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })
          (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))
match s.findMin le (cons r a c) ⟨id, a, c, s⟩ with
| { before, val, node, next } =>
  intro ⟨⟨_, hk, ih₁, ih₂⟩⟩
  exact ih₁.toHeap.merge <| hk (ih₂.of_le (Nat.le_succ _))
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
rank✝ : Nat
hk :
  ∀ {s : Heap α},
    WellFormed le rank✝ s →
      WellFormed le 0 (FindMin.before { before := before, val := val, node := node, next := next } s)
ih₁ :
  HeapNode.WellFormed le { before := before, val := val, node := node, next := next }.val
    { before := before, val := val, node := node, next := next }.node rank✝
ih₂ : WellFormed le (rank✝ + 1) { before := before, val := val, node := node, next := next }.next
⊢ WellFormed le 0
    (Heap.merge le (HeapNode.toHeap { before := before, val := val, node := node, next := next }.node)
      (FindMin.before { before := before, val := val, node := node, next := next }
        { before := before, val := val, node := node, next := next }.next))
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
⊢ Nonempty (FindMin.WellFormed le { before := before, val := val, node := node, next := next }) →
    WellFormed le 0
      (Heap.merge le (HeapNode.toHeap { before := before, val := val, node := node, next := next }.node)
        (FindMin.before { before := before, val := val, node := node, next := next }
          { before := before, val := val, node := node, next := next }.next))
intro ⟨⟨_, hk, ih₁, ih₂⟩⟩
no goals
α : Type u_1
le : α → α → Bool
n r : Nat
a : α
c : HeapNode α
s : Heap α
h : WellFormed le n (cons r a c s)
before : Heap α → Heap α
val : α
node : HeapNode α
next : Heap α
rank✝ : Nat
hk :
  ∀ {s : Heap α},
    WellFormed le rank✝ s →
      WellFormed le 0 (FindMin.before { before := before, val := val, node := node, next := next } s)
ih₁ :
  HeapNode.WellFormed le { before := before, val := val, node := node, next := next }.val
    { before := before, val := val, node := node, next := next }.node rank✝
ih₂ : WellFormed le (rank✝ + 1) { before := before, val := val, node := node, next := next }.next
⊢ WellFormed le 0
    (Heap.merge le (HeapNode.toHeap { before := before, val := val, node := node, next := next }.node)
      (FindMin.before { before := before, val := val, node := node, next := next }
        { before := before, val := val, node := node, next := next }.next))
exact ih₁.toHeap.merge <| hk (ih₂.of_le (Nat.le_succ _))