induction h with
| node_next_left x i y hi _ hr hx' hx h _ =>
  rewrite [h.get_not_descendant i (fun h => Nat.not_lt_of_le h.le (lt_child_left i))]
  have ⟨k,hk,hdk,h⟩ := h.exists_get_descendant (2*i+1) hl (.refl  _)
  rewrite [Subarray.getElem_swap_left, h, Subarray.getElem_swap]
  if hlk : 2*i+1 = k then
    simp only [if_pos hlk]; exact LawfulLTBRel.asymm hx
  else
    simp only [if_neg hlk, if_neg <| Nat.ne_of_lt <| trans (lt_child_left i) hdk.le]
    exact heap_left.not_lt_of_descendant k hdk
| node_end_left x i _ _ _ _ hx =>
  exact hx
| node_next_right x i y hi _ hr hx' hx h _ =>
  rewrite [h.get_not_descendant i (fun h => Nat.not_lt_of_le h.le (lt_child_right i))]
  rewrite [h.get_not_descendant (2*i+1) (Descendant.sibling_not' i)]
  rw [Subarray.getElem_swap_left, Subarray.getElem_swap_ne, hx']
  . show i ≠ 2*i+1; exact Nat.ne_of_lt (lt_child_left i)
  . show 2*i+1+1 ≠ 2*i+1; exact Nat.ne_of_gt .refl
| node_end_right x i hi _ hr hx' hx =>
  exact LawfulLTBRel.ntrans hx hx'
| node_odd_next x i hi _ hr hx =>
  rewrite [Subarray.getElem_swap_left, Subarray.getElem_swap_right]
  exact LawfulLTBRel.asymm hx
| node_odd_end x i _ _ _ hx =>
  exact hx
| leaf x i  hl' => exact absurd hl <| Nat.not_lt_of_le hl'
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
hl : 2 * i + 1 < Subarray.size x
heap_left : IsHeap lt x (2 * i + 1)
⊢ lt y[i] y[2 * i + 1] = false
no goals