induction h with
| out_of_range i hi =>
  exact .out_of_range i <| Nat.le_trans hsize hi
| node' i _ lt_left lt_right _ _ IH₁ IH₂ =>
  specialize IH₁ fun k hk h => hext k hk (.node_left _ h)
  specialize IH₂ fun k hk h => hext k hk (.node_right _ h)
  if hiy : i < y.size then
    refine .node' i hiy ?_ ?_ IH₁ IH₂
    . intro hl
      rewrite [hext i hiy (.refl i), hext (2*i+1) hl (.child_left i)]
      exact lt_left <| Nat.lt_of_lt_of_le hl hsize
    . intro hr
      rewrite [hext i hiy (.refl i), hext (2*i+2) hr (.child_right i)]
      exact lt_right <| Nat.lt_of_lt_of_le hr hsize
  else
    exact .out_of_range i (Nat.le_of_not_lt hiy)
α : Type u
lt : α → α → Bool
x y : Subarray α
i : Nat
h : IsHeap lt x i
hsize : Subarray.size y ≤ Subarray.size x
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
⊢ IsHeap lt y i
no goals