cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hjk) with
| inl heq =>
  cases heq
  have : i.1 ≤ l :=
    Nat.le_of_succ_le_succ (Or.resolve_right hil j.1.lt_irrefl)
  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'
| inr hlt =>
  specialize IH' (Or.inr hlt)
  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
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)
IH' : ↑i < l ∨ ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ invs'
hil : ↑i < l + 1 ∨ ↑j < k
⊢ { 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