if hx' : lt x[rhs] x[lhs] then
  have hjl : j = lhs := if_pos hx'
  simp (config:={zeta:=false}) only [hjl] at IH ⊢
  if hx : lt x[i] x[lhs] then
    simp only [if_pos hx]
    exact node_next_left x i _ hi hl hr hx' hx IH
  else
    simp only [if_neg hx]
    exact node_end_left x i hi hl hr hx' (Bool.of_not_eq_true hx)
else
  have hjr : j = rhs := if_neg hx'
  simp (config:={zeta:=false}) only [hjr] at IH ⊢
  if hx : lt x[i] x[rhs] then
    simp only [if_pos hx]
    exact node_next_right x i _ hi hl hr (Bool.of_not_eq_true hx') hx IH
  else
    simp only [if_neg hx]
    exact node_end_right x i hi hl hr (Bool.of_not_eq_true hx') (Bool.of_not_eq_true hx)
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
no goals