. rename_i xs₂ t₁ ts hne₂ heqh
  rw[Option.some_inj] at dmeq
  unfold findMin at dmeq
  split at dmeq
  . contradiction
  . split at dmeq
    . simp at *
      rename_i ts n btxn bt ts₂ bt₂ n₂ lebt eqeq
      rw[←dmeq.right]
      apply And.intro
      . unfold merge
        split
        rename_i ys₂ xs₃ ts₃ ts₄ heq heq₂
        simp at heq
        unfold List.eraseIdx at heq
        have ihts₃ : IsHeap (.heap ts₃) := by
          split at heq
          . simp_all
          . simp_all
            unfold IsHeap
            simp
            unfold IsHeapForest
            cases h₁
            apply IsHeapForest'_weaken
            . assumption
            . simp_arith
          . rename_i heq₃ _
            rw[← heq]
            apply IsHeap_delete_BinTree
            rw[← heq₃, ← heqh.left, ← heqh.right] 
            assumption
        have ihts₄ : IsHeap (.heap ts₄) := by
          clear heq 
          rw [← heq₂]
          have (And.intro ml mr) := eqeq
          rw [← ml, ← mr] at *; clear eqeq ml mr
          apply children_IsHeap
          constructor
          . have fm : IsBinTree (findMin le ts₂ (1 + 1) (t₁, 0)).fst := by
              apply IsBinTree_findMin
              . cases h₁ with | cons _ _ hf =>
                rw[heqh.right] at hf 
                cases hf
                assumption
              . cases h₁
                simp_all
            apply min_rank_IsBinTree 
            assumption
          . apply IsBinTree_findMin
            . rw[heqh.right] at h₁
              cases h₁ with | cons _ _ hf =>
                cases hf
                assumption
            . unfold IsHeap at h₁
              unfold IsHeapForest at h₁
              cases h₁ with | cons _ ht _ =>
              rw[heqh.left] at ht
              assumption
          . constructor
        unfold IsHeap at *
        unfold IsHeapForest at *
        simp at *
        have min_zero : 0 = min 0 0 := by
          simp
        rw[min_zero]
        apply IsHeap_merge <;> assumption
      . unfold merge
        split
        rename_i ys₂ xs₃ ts₃ ts₄ heq heq₂
        simp at heq
        unfold List.eraseIdx at heq
        have h₁₂ : IsMinHeap le (.heap ts₃) := by
          split at heq
          . rw[← heq]
            constructor
          . rename_i ts₅ heq₃ _
            rw[← heqh.right] at heq₃
            have eq : hs = ts₅ := by
              apply List.tail_eq_of_cons_eq
              assumption
            rw[← heq, ← eq]
            cases h₂
            assumption
          . rename_i heq₃ _
            rw[← heq]
            apply IsMinHeap_delete_BinTree
            rw[← heq₃, ← heqh.left, ← heqh.right]
            assumption                                                           
        have h₁₃ : IsMinHeap le (.heap ts₄) := by
          rw[← heq₂]
          apply children_IsMinHeap
          constructor
          . apply IsSearchTree_findMin
            . rw[heqh.right] at h₂
              cases h₂ with | cons _ mh => 
              cases mh
              assumption
            . rw[← eqeq.left, ← heqh.left]
              cases h₂
              assumption
          . constructor
        apply IsMinHeap_merge
        simp
        repeat assumption
    . simp at dmeq
      have (And.intro _ heq) := dmeq
      clear dmeq
      unfold merge at heq
      split at heq
      rename_i bt ts _ _ _ _ _ _ _ ts₂ ts₃ heq₃ heq₄
      rw[← heq]
      apply And.intro
      . have ihts₂ : IsHeap (.heap ts₂) := by
          rw[← heq₃]
          unfold IsHeap
          unfold IsHeapForest
          apply IsHeapForest'_eraseIdx
          simp at heqh
          constructor
          . apply min_rank_IsBinTree
            rw[← heqh.left]
            cases h₁
            assumption
          . rw[← heqh.left]
            cases h₁
            assumption
          . cases h₁
            rw[← heqh.left, ← heqh.right]
            assumption
        have h₂₄ : IsHeap (.heap ts₃) := by
          rw[← heq₄]
          apply children_IsHeap
          constructor
          . have ibt : IsBinTree (findMin le ts (1 + 1) (bt, 1)).fst := by
              simp at heqh
              rw[heqh.right] at h₁
              apply IsBinTree_findMin <;>
                cases h₁ with | cons _ _ hf =>
                cases hf
                assumption
            apply min_rank_IsBinTree ibt
          . simp at heqh
            rw[heqh.right] at h₁
            apply IsBinTree_findMin <;>
              cases h₁ with | cons _ _ hf =>
              cases hf
              assumption
          . constructor
        unfold IsHeap at *
        unfold IsHeapForest at *
        simp at *
        have min_zero : 0 = min 0 0 := by
          simp
        rw[min_zero]
        apply IsHeap_merge <;> assumption
      . simp at heqh
        have imhts₂ : IsMinHeap le (.heap ts₂) := by
          rw[← heq₃]
          apply IsMinHeap_eraseIdx
          rw[← heqh.left, ← heqh.right]
          assumption
        have imhts₃ : IsMinHeap le (.heap ts₃) := by
          rw[← heq₄]
          apply children_IsMinHeap
          constructor
          . apply IsSearchTree_findMin <;>
            . rw[heqh.right] at h₂
              cases h₂ with | cons _ mh =>
              cases mh
              assumption
          . constructor
        apply IsMinHeap_merge <;> assumption
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
xs : Heap α
y : α
ys : Heap α
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
h₁ : IsHeap (Heap.heap (h :: hs))
h₂ : IsMinHeap le (Heap.heap (h :: hs))
x✝¹ : Heap α
h✝ : HeapNodeAux α (Heap α)
hs✝ : List (HeapNodeAux α (Heap α))
x✝ : hs✝ = [] → False
heq✝ : Heap.heap (h :: hs) = Heap.heap (h✝ :: hs✝)
dmeq :
  some
      ((findMin le hs✝ 1 (h✝, 0)).fst.val,
        merge le (Heap.heap (List.eraseIdx (h✝ :: hs✝) (findMin le hs✝ 1 (h✝, 0)).snd))
          (findMin le hs✝ 1 (h✝, 0)).fst.children) =
    some (y, ys)
⊢ IsHeap ys ∧ IsMinHeap le ys
no goals