induction h with
| node_next_left x i y hi hl hr hx' hx _ IH =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_pos hx', if_pos hx]
  exact IH
| node_end_left x i hi hl hr hx' hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_pos hx', if_neg (Bool.eq_false_iff.mp hx)]
| node_next_right x i y hi hl hr hx' hx _ IH =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_pos hx]
  exact IH
| node_end_right x i hi hl hr hx' hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_neg (Bool.eq_false_iff.mp hx)]
| node_odd_next x i hi hl hr hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_neg (Nat.not_lt_of_le hr), dif_pos hl, if_pos hx]
| node_odd_end x i hi hl hr hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_neg (Nat.not_lt_of_le hr), dif_pos hl, if_neg (Bool.eq_false_iff.mp hx)]
| leaf x i hl =>
  have hr : 2*i+2 ≥ x.size := .step hl
  unfold heapifyDown heapifyDownAux
  simp only [dif_neg (Nat.not_lt_of_le hr), dif_neg (Nat.not_lt_of_le hl)]
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
⊢ y = heapifyDown lt x i
no goals