. intro hl'; exact absurd hl' (Nat.not_lt_of_le hl)
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false