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