simp only [hx, if_pos, dif_pos, Array.size_push]
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
i : Fin ↑j
ivs' : Array (Inversion x)
hx : x[↑i] > x[↑j]
⊢ (if x[↑i] > x[↑j] then Array.size ivs' + 1 else Array.size ivs') =
    Array.size
      (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')
no goals