cases Nat.lt_or_eq_of_le x.h₁ with
| inl hlt =>
  simp only [dif_pos hlt, size_heapifyDown, Subarray.size_shrinkOne', Subarray.size_swap]
| inr heq =>
  rewrite [dif_neg (c:=x.start < x.stop) (heq ▸ x.start.lt_irrefl)]
  simp only [Subarray.size, heq, x.stop.sub_self]
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Subarray.size
      (if h : x.start < x.stop then
        let_fun this := (_ : 0 < x.stop - x.start);
        let x :=
          Subarray.swap x { val := 0, isLt := this }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
        heapifyDown lt (Subarray.shrinkOne' x h) 0
      else x) =
    Subarray.size x - 1
no goals