simp
α : Type u_1
le : α → α → Bool
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
xs : Heap α
y : α
ys : Heap α
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
h₁ : IsHeapForest' 0 (h :: hs)
h₂ : IsMinHeap le (Heap.heap (h :: hs))
xs₂ : Heap α
t₁ : HeapNodeAux α (Heap α)
x✝⁴ : List (BinTree α)
x✝³ : ℕ
x✝² : BinTree α × ℕ
bt : BinTree α
ts : List (BinTree α)
h'✝ : BinTree α
idx'✝ : ℕ
left✝ : (findMin le ts (1 + 1) (bt, 1)).fst.val = y
x✝¹ x✝ : Heap α
ts₂ ts₃ : List (HeapNodeAux α (Heap α))
heq₄ : (findMin le ts (1 + 1) (bt, 1)).fst.children = Heap.heap ts₃
heq : Heap.heap (mergeNodes le ts₂ ts₃) = ys
ihts₂ : IsHeapForest' 0 ts₂
h₂₄ : IsHeapForest' 0 ts₃
not_le_le : ∀ (x y : α), le x y = false → le y x = true
heq✝ : t₁ = h'✝ ∧ 0 = idx'✝
hne₂ : True
heqh : h = t₁ ∧ hs = bt :: ts
h✝ : le h'✝.val bt.val = false
heq₃ : List.eraseIdx (t₁ :: bt :: ts) (findMin le ts (1 + 1) (bt, 1)).snd = ts₂
⊢ 0 = min 0 0
no goals