intro j _
case H
n : Nat
x : Permutation n
⊢ ∀ (i : Fin n) (a : Array (Inversion x)),
    Nat.fold' (↑i) (fun i_1 k => if x[↑i_1] > x[↑i] then k + 1 else k) (Array.size a) =
      Array.size
        (Nat.fold' (↑i)
          (fun i_1 ivs =>
            if h : x[↑i_1] > x[↑i] then
              Array.push ivs { fst := Fin.castLE (_ : ↑i ≤ n) i_1, snd := i, lt := (_ : ↑i_1 < ↑i), inverted := h }
            else ivs)
          a)
case H
n : Nat
x : Permutation n
j : Fin n
a✝ : Array (Inversion x)
⊢ Nat.fold' (↑j) (fun i k => if x[↑i] > x[↑j] then k + 1 else k) (Array.size a✝) =
    Array.size
      (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)
        a✝)