if h : x.start < x.stop then
  simp only [dif_pos h]
  rewrite [get_as_heapifyDown_of_ge_stop lt _ 0 i]
  . simp only [Subarray.as_shrinkOne']
    refine Array.getElem_swap_ne x.as _ _ _ ?_ ?_
    . exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
    . exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
  . simp only [Subarray.stop_shrinkOne']
    exact Nat.le_trans x.stop.pred_le hge
else
  simp only [dif_neg h]
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
⊢ (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).as[i] =
    x.as[i]
no goals