refine Nat.fold'_induction (motive := fun k (ivs : Array (Inversion x)) => j.1 < k → ⟨i,j,hlt,hinv⟩ ∈ ivs) n _ #[] ?zero ?succ j.2
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
    Nat.fold' n
      (fun j =>
        Nat.fold' ↑j fun i ivs =>
          if h : x[↑i] > x[↑j] then
            Array.push ivs { fst := Fin.castLE (_ : ↑j ≤ n) i, snd := j, lt := (_ : ↑i < ↑j), inverted := h }
          else ivs)
      #[]
case zero
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) 0 #[]

case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) i_1 a →
      (fun k ivs => ↑j < k → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ ivs) (i_1 + 1)
        (Nat.fold' (↑{ val := i_1, isLt := hi })
          (fun i ivs =>
            if h : x[↑i] > x[↑{ val := i_1, isLt := hi }] then
              Array.push ivs
                { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                  lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
            else ivs)
          a)