dsimp [inversionNum, inversions]
n : Nat
x : Permutation n
⊢ inversionNum x = Array.size (inversions x)
n : Nat
x : Permutation n
⊢ Nat.fold' n (fun j => Nat.fold' ↑j fun i k => if x[↑i] > x[↑j] then k + 1 else k) 0 =
    Array.size
      (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)
        #[])