. have : u.rank ≠ c.rank := by
    apply ne_of_lt
    assumption
  contradiction
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : u.rank < c.rank
⊢ u.rank + 1 ≤ hRank (u :: mergeNodes le y (c :: z))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : ¬u.rank < c.rank
⊢ u.rank + 1 ≤
    hRank
      (if c.rank < u.rank then c :: mergeNodes le z (u :: y)
      else
        let merged := combine le u c;
        let r := merged.rank;
        if (r != hRank y) = true then
          if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
        else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝ : ¬u.rank < c.rank
⊢ u.rank + 1 ≤
    hRank
      (if c.rank < u.rank then c :: mergeNodes le z (u :: y)
      else
        let merged := combine le u c;
        let r := merged.rank;
        if (r != hRank y) = true then
          if (r != hRank z) = true then merged :: mergeNodes le y z else mergeNodes le (merged :: y) z
        else if (r != hRank z) = true then mergeNodes le y (merged :: z) else merged :: mergeNodes le y z)