induction h with
| out_of_range _ h => refine .out_of_range _ h
| node' i hi hx₁ hx₂ _ _ IHl IHr =>
  specialize IHl (trans hj₁ (lt_child_left i)) (trans hj₂ (lt_child_left i))
  specialize IHr (trans hj₁ (lt_child_right i)) (trans hj₂ (lt_child_right i))
  refine node' i hi ?_ ?_ IHl IHr
  . intro hl; specialize hx₁ hl
    simp only [Subarray.getElem_swap]
    iterate rewrite [if_neg]
    exact hx₁
    all_goals apply Nat.ne_of_lt
    . exact trans hj₁ (lt_child_left i)
    . exact trans hj₂ (lt_child_left i)
    . exact hj₁
    . exact hj₂
  . intro hr; specialize hx₂ hr
    simp only [Subarray.getElem_swap]
    iterate rewrite [if_neg]
    exact hx₂
    all_goals apply Nat.ne_of_lt
    . exact trans hj₁ (lt_child_right i)
    . exact trans hj₂ (lt_child_right i)
    . exact hj₁
    . exact hj₂
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
h : IsHeap lt x i
j₁ j₂ : Fin (Subarray.size x)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
no goals