. split
  . constructor
    . cases hys
      assumption
    . cases hys
      apply IsMinHeap_merge <;> assumption
  . dsimp
    split
    . split
      . constructor
        . apply combine_IsSearchTree
          . assumption
          . cases hxs
            assumption
          . cases hys
            assumption
        . apply IsMinHeap_merge
          . cases hxs
            assumption
          . cases hys
            assumption
      . apply IsMinHeap_merge
        . constructor
          . apply combine_IsSearchTree
            . assumption
            . cases hxs
              assumption
            . cases hys
              assumption
          . cases hxs
            assumption
        . cases hys
          assumption
    . split
      . apply IsMinHeap_merge
        . cases hxs
          assumption
        . constructor
          . apply combine_IsSearchTree
            . assumption
            . cases hxs
              assumption
            . cases hys
              assumption
          . cases hys
            assumption
      . constructor
        . apply combine_IsSearchTree
          . assumption
          . cases hxs
            assumption 
          . cases hys
            assumption
        . apply IsMinHeap_merge
          . cases hxs
            assumption
          . cases hys
            assumption
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
h✝ : ¬h₁.rank < h₂.rank
⊢ IsMinHeap le
    (Heap.heap
      (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂))
no goals