intro k hk ivs ivs_nodup ivs_lt
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
case refine_2
n : Nat
x : Permutation n
k : Nat
hk : k < n
ivs : Array (Inversion x)
ivs_nodup : Array.Nodup ivs
ivs_lt : ∀ (iv : Inversion x), iv ∈ ivs → ↑iv.snd < k
⊢ Array.Nodup
      (Nat.fold' k
        (fun i ivs =>
          if h : x[↑i] > x[k] then
            Array.push ivs
              { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
                lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
          else ivs)
        ivs) ∧
    ∀ (iv : Inversion x),
      iv ∈
          Nat.fold' k
            (fun i ivs =>
              if h : x[↑i] > x[k] then
                Array.push ivs
                  { fst := Fin.castLE (_ : ↑{ val := k, isLt := hk } ≤ n) i, snd := { val := k, isLt := hk },
                    lt := (_ : ↑i < ↑{ val := k, isLt := hk }), inverted := h }
              else ivs)
            ivs →
        ↑iv.snd < k + 1