cases Nat.lt_or_eq_of_le x.h₁ with
| inl hrng =>
  simp only [stop_popMax lt x hrng] at hi
  have stop_pos : 0 < x.stop :=
    Nat.lt_of_le_of_lt x.start.zero_le hrng
  have : x.stop-1+1 = x.stop :=
    Nat.sub_add_cancel stop_pos
  have hj' : x.stop ≤ j :=
    trans this.symm (trans hi hij :)
  rewrite [get_as_popMax_of_ge_stop lt x j hj']
  cases Nat.lt_or_eq_of_le hi with
  | inl hlti =>
    have : x.stop ≤ i :=
      ‹x.stop-1+1=x.stop› ▸ (hlti : x.stop-1+1 ≤ i)
    rewrite [get_as_popMax_of_ge_stop lt x i this]
    exact h.sorted i j this hij hj
  | inr heqi =>
    cases heqi
    rewrite [get_as_popMax_stop_sub_one lt x hrng]
    exact h.bound_above j 0 ⟨hj',hj⟩ _
| inr hz =>
  simp only [popMax_empty lt x hz] at hi ⊢
  exact h.sorted i j hi hij hj
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i
hij : i < j
hj : j < stop
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
no goals