simp only [Subarray.size_shrinkOne', Subarray.size_swap]
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ i <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this✝ : i + 1 < x.stop - x.start
this : x.start < x.stop
hzero : 0 < Subarray.size x
hlast : Subarray.size x - 1 < Subarray.size x
⊢ i < Subarray.size x - 1