simp only [this] at *
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝³ : ((combine le h₁ h₂).rank != hRank t₁) = true
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝² : h₂.rank ≤ h₁.rank
h✝¹ : h₁.rank ≤ h₂.rank
h✝ : ((combine le h₁ h₂).rank != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
this : (combine le h₁ h₂).rank = h₁.rank + 1
⊢ IsHeapForest' (combine le h₁ h₂).rank t₁
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝¹ : rx < h₁.rank
a✝ : IsBinTree h₁
hf : IsHeapForest' h₁.rank t₁
h✝¹ : (h₁.rank + 1 != hRank t₁) = true
h✝ : (h₁.rank + 1 != hRank t₂) = false
this : True
⊢ IsHeapForest' (h₁.rank + 1) t₁