dsimp [inversions]
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 } ∈ inversions x
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)
      #[]