rw[hrank_of_cons]
case inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
⊢ min h₁.rank h₂.rank ≤ hRank (h₂ :: mergeNodes le t₂ (h₁ :: t₁))
case inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
xs ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
ht₁ : IsHeapForest' r (h₁ :: t₁)
ht₂ : IsHeapForest' r (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
⊢ min h₁.rank h₂.rank ≤ h₂.rank