clear h
α : 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
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
h :
  (heapifyDown lt
        (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
          this)
        0)[i] =
    (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)[k]
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]
α : 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
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne' (Subarray.swap x { val := 0, isLt := hzero } { val := Subarray.size x - 1, isLt := hlast })
        this)
⊢ ∃ k_1 hk_1,
    0 < k_1 ∧ (if Subarray.size x - 1 = k then x[0] else if 0 = k then x[Subarray.size x - 1] else x[k]) = x[k_1]