. 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
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap 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) })
      hsize)
    (2 * 0 + 2)
no goals