have : i.1 ≤ l :=
  Nat.le_of_succ_le_succ (Or.resolve_right hil j.1.lt_irrefl)
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
⊢ { 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'
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'