exact _hdecreasing
α : Type u
lt : α → α → Bool
_x✝ : (_ : Subarray α) ×' Nat
a✝¹ :
  ∀ (y : (_ : Subarray α) ×' Nat),
    (invImage (fun a => PSigma.casesOn a fun x snd => Subarray.size x - snd) instWellFoundedRelation).1 y _x✝ →
      heapifyDown.OpSpec lt y.1 y.2 (heapifyDown lt y.1 y.2)
x : Subarray α
i : Nat
a✝ :
  ∀ (y : (_ : Subarray α) ×' Nat),
    (invImage (fun a => PSigma.casesOn a fun x snd => Subarray.size x - snd) instWellFoundedRelation).1 y
        { fst := x, snd := i } →
      heapifyDown.OpSpec lt y.1 y.2 (heapifyDown lt y.1 y.2)
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
j : Nat := if h : lt x[rhs] x[lhs] = true then lhs else rhs
_hdecreasing : Subarray.size x - j < Subarray.size x - i
⊢ (invImage (fun a => PSigma.casesOn a fun x snd => Subarray.size x - snd) instWellFoundedRelation).1
    {
      fst :=
        Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) } { val := j, isLt := (_ : j < Subarray.size x) },
      snd := j }
    { fst := x, snd := i }
no goals