all_goals simp
case refine_1
n : Nat
x : Permutation n
⊢ (fun k ivs => Array.Nodup ivs ∧ ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k) 0 #[]

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

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