. exact Nat.ne_of_lt hki.le
case refine_1.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (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)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k

case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (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)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (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)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k