. rename_i heq
  rw[← List.tail_eq_of_cons_eq heq]
  assumption
case h_2
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
head✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
heq✝ : t :: ts = head✝ :: as✝
⊢ IsMinHeap le (Heap.heap as✝)

case h_3
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
a✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsMinHeap le (Heap.heap (a✝ :: List.eraseIdx as✝ n✝))
case h_3
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
a✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsMinHeap le (Heap.heap (a✝ :: List.eraseIdx as✝ n✝))