if hr : rhs < x.size then
  simp (config:={zeta:=false,beta:=false}) only [dif_pos hr]
  takeout_lets; iterate intro_let
  have _hdecreasing := ‹x.size - j < x.size - i›
  have IH := OpSpec.mk (x.swap ⟨i,hi⟩ ⟨j,hj.2⟩) j
  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)
else if hl : lhs < x.size then
  simp (config:={zeta:=false,beta:=false}) only [dif_neg hr, dif_pos hl]
  takeout_lets; intro_let
  if hx : lt x[i] x[lhs] then
    simp only [if_pos hx]
    exact node_odd_next x i hi hl (Nat.le_of_not_lt hr) hx
  else
    simp only [if_neg hx]
    exact node_odd_end x i hi hl (Nat.le_of_not_lt hr) (Bool.of_not_eq_true hx)
else
  simp only [dif_neg hr, dif_neg hl]
  exact leaf x i (Nat.le_of_not_lt hl)
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
⊢ heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
no goals