all_goals simp only [Subarray.as_shrinkOne', Subarray.as_swap, Subarray.start_shrinkOne', Subarray.start_swap]
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
          (_ : x.start < x.stop)).as[i] =
    x.as[i]

α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i <
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).start
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ (Array.swap x.as (Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) })
        (Subarray.castIndex x
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }))[i] =
    x.as[i]

α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i < x.start