have : i.1 < k := trans (r:=LT.lt (α:=Nat)) hlt (Nat.le_of_succ_le_succ hjk)
case succ
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
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Nat.fold' k
      (fun i ivs =>
        if h : x[↑i] > x[k] then
          Array.push ivs
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
              lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
        else ivs)
      invs
case succ
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
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Nat.fold' k
      (fun i ivs =>
        if h : x[↑i] > x[k] then
          Array.push ivs
            { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
              lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
        else ivs)
      invs