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