induction h with
| node_next_left x i y hi hl hr hx' hx h IH =>
  refine .node lt y i (h.size_eq ▸ hr) (_hy_left hl) (_hy_right hr) ?_ ?_
  . show IsHeap lt y (2*i+1)
    refine IH ?_ ?_
    . refine heap_left.left.swap _ _ ?_ (lt_child_left (2*i+1))
      exact trans (lt_child_left i) (lt_child_left (2*i+1))
    . refine heap_left.right.swap _ _ ?_ (lt_child_right (2*i+1))
      exact trans (lt_child_left i) (lt_child_right (2*i+1))
  . show IsHeap lt y (2*i+2)
    refine heap_right.of_subext (h.size_eq ▸ .refl) ?_
    intro k hk hdk
    rw [h.get_not_descendant k fun h => Descendant.sibling_not i <| h.ascend_right (.step .refl) hdk, Subarray.getElem_swap_ne]
    . exact Nat.ne_of_lt <| trans (lt_child_right i) hdk.le
    . exact Nat.ne_of_lt <| trans (2*i+1).lt_succ_self hdk.le
| node_end_left x i _ hl hr hx' hx =>
  refine .node lt x i hr hx ?_ heap_left heap_right
  exact LawfulLTBRel.ntrans hx <| LawfulLTBRel.asymm hx'
| node_next_right x i y hi hl hr hx' hx h IH =>
  refine .node lt y i (h.size_eq ▸ hr) (_hy_left hl) (_hy_right hr) ?_ ?_
  . show IsHeap lt y (2*i+1)
    refine heap_left.of_subext (h.size_eq ▸ .refl) ?_
    intro k hk hdk
    rw [h.get_not_descendant k fun h => Descendant.sibling_not i <| hdk.ascend_right (.step .refl) h, Subarray.getElem_swap_ne]
    . exact Nat.ne_of_lt <| trans (lt_child_left i) hdk.le
    . dsimp; intro h; cases h; exact absurd hdk (Descendant.sibling_not i)
  . show IsHeap lt y (2*i+2)
    refine IH ?_ ?_
    . refine heap_right.left.swap _ _ ?_ (lt_child_left (2*i+2))
      exact trans (lt_child_right i) (lt_child_left (2*i+2))
    . refine heap_right.right.swap _ _ ?_ (lt_child_right (2*i+2))
      exact trans (lt_child_right i) (lt_child_right (2*i+2))
| node_end_right x i _ _ hr hx' hx =>
  exact .node lt x i hr (LawfulLTBRel.ntrans hx hx') hx heap_left heap_right
| node_odd_next x i hi hl hr hx =>
  refine .node_odd lt _ i hl hr ?_
  rewrite [Subarray.getElem_swap_left, Subarray.getElem_swap_right]
  exact LawfulLTBRel.asymm hx
| node_odd_end x i _ hl hr hx =>
  exact .node_odd lt x i hl hr hx
| leaf x i hl => exact .leaf lt x i hl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false := fun hl => not_lt_left h hl heap_left
_hy_right : ∀ (hr : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false := fun hr => not_lt_right h hr heap_right
⊢ IsHeap lt y i
no goals