cases Nat.eq_or_lt_of_le this with
| inl heq =>
  cases heq; rewrite [dif_pos hinv]
  exact Array.mem_push.mpr <| Or.inr rfl
| inr hlt =>
  specialize IH' (Or.inl hlt)
  if hx : x[l]'(Nat.lt_trans hl j.2) > x[j.1] then
    rewrite [dif_pos hx]
    exact Array.mem_push.mpr <| Or.inl IH'
  else
    rewrite [dif_neg hx]; exact IH'
case succ.refine_2.inl.refl
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
invs : Array (Inversion x)
l : Nat
invs' : Array (Inversion x)
hk : ↑j < n
IH : ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs
hjk : ↑j < ↑j + 1
this✝ : ↑i < ↑j
hl : l < ↑j
IH' : ↑i < l ∨ ↑j < ↑j → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < ↑j
this : ↑i ≤ l
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    if h : x[l] > x[↑j] then
      Array.push invs'
        { fst := { val := l, isLt := (_ : l < n) }, snd := { val := ↑j, isLt := hk },
          lt := (_ : { val := l, isLt := (_ : l < n) } < { val := ↑j, isLt := hk }),
          inverted := (_ : x[↑{ val := l, isLt := (_ : l < n) }] > x[↑{ val := ↑j, isLt := hk }]) }
    else invs'
no goals