if hsize : x.start < x.stop then
  simp only [dif_pos hsize]
  refine is_heap_heapifyDown lt _ 0 ?_ ?_
  . refine h.left.of_subext ?_ ?_
    . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
    . intro k hk hki
      rewrite [Subarray.getElem_shrinkOne']
      refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
      . exact Nat.ne_of_lt hki.le
      . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
        simp only [Subarray.size_shrinkOne', Subarray.size_swap]
        exact .refl
  . refine h.right.of_subext ?_ ?_
    . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
    . intro k hk hki
      refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
      . exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
      . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
        simp only [Subarray.size_shrinkOne', Subarray.size_swap]
        exact .refl
else
  simp only [dif_neg hsize]; exact h
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
⊢ IsHeap lt
    (if h : x.start < x.stop then
      heapifyDown lt
        (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
          h)
        0
    else x)
    0
no goals