have : x.start < x.stop := calc
  x.start < i+1+x.start := Nat.lt_add_of_pos_left i.zero_lt_succ
  _       < x.stop := Nat.add_lt_of_lt_sub this
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
this : i + 1 < x.stop - x.start
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown 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) })
                h)
              0
          else x)[i] =
        x[k]
α : 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
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            heapifyDown 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) })
                h)
              0
          else x)[i] =
        x[k]