. dsimp
  simp
  simp_all
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
h✝ : le t₂.val t₁.val = true
⊢ { val := t₂.val, rank := t₂.rank + 1, children := Heap.heap (Heap.nodes t₂.children ++ [t₁]) }.rank = t₁.rank + 1

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
h✝ : ¬le t₂.val t₁.val = true
⊢ { val := t₁.val, rank := t₁.rank + 1, children := Heap.heap (Heap.nodes t₁.children ++ [t₂]) }.rank = t₁.rank + 1
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
t₁ t₂ : BinTree α
a✝ : t₁.rank = t₂.rank
h✝ : ¬le t₂.val t₁.val = true
⊢ { val := t₁.val, rank := t₁.rank + 1, children := Heap.heap (Heap.nodes t₁.children ++ [t₂]) }.rank = t₁.rank + 1