rw[Nat.min_eq]
case inr.inr.inl.inr.a
α : Type u_1
le : α → α → Bool
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 + 1 != hRank t₁) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
hf₂ : IsHeapForest' r t₂
ih : min (h₁.rank + 1) (hRank t₂) ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ min (h₁.rank + 1) (hRank t₂)
case inr.inr.inl.inr.a
α : Type u_1
le : α → α → Bool
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 + 1 != hRank t₁) = true
hf : IsHeapForest' r (combine le h₁ h₂ :: t₁)
hf₂ : IsHeapForest' r t₂
ih : min (h₁.rank + 1) (hRank t₂) ≤ hRank (mergeNodes le (combine le h₁ h₂ :: t₁) t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
⊢ (if h₁.rank ≤ h₂.rank then h₁.rank else h₂.rank) ≤ if h₁.rank + 1 ≤ hRank t₂ then h₁.rank + 1 else hRank t₂