. intro k hk ivs ivs_nodup ivs_lt
  generalize hivs' : Nat.fold' k _ ivs = ivs'
  suffices Array.Nodup ivs' ∧ ∀ iv, iv ∈ ivs' → iv.snd.1 < k ∨ (iv.snd.1 = k ∧ iv.fst.1 < k) by
    refine And.imp_right ?_ this
    intro hivs' iv hiv
    apply Nat.succ_le_succ; apply Nat.le_iff_lt_or_eq.mpr
    exact Or.imp_right And.left (hivs' iv hiv)
  cases hivs'
  refine Nat.fold'_induction (motive := fun l (ivs' : Array (Inversion x)) => ivs'.Nodup ∧ ∀ iv, iv ∈ ivs' → iv.snd.1 < k ∨ (iv.snd.1 = k ∧ iv.fst.1 < l)) k _ ivs ?_ ?_
  all_goals simp
  . exact And.intro ivs_nodup fun iv hiv => Or.inl <| ivs_lt iv hiv
  . intro l hl ivs' ivs'_nodup ivs'_lt
    if hx : x[l]'(Nat.lt_trans hl hk) > x[k] then
      simp only [dif_pos hx, Array.nodup_push, Array.mem_push, ivs'_nodup, true_and]
      constructor
      . intro h
        specialize ivs'_lt _ h; dsimp at ivs'_lt
        refine ivs'_lt.elim ?_ ?_
        . exact Nat.lt_irrefl k
        . intro h; exact Nat.lt_irrefl l h.2
      . intro iv hiv
        cases hiv with
        | inl hmem =>
          refine Or.imp_right ?_ <| ivs'_lt iv hmem
          exact And.imp_right Nat.le.step
        | inr heq =>
          cases heq; dsimp
          exact Or.inr ⟨rfl, l.lt_succ_self⟩
    else
      simp only [dif_neg hx]
      apply And.intro ivs'_nodup
      intro iv hiv; specialize ivs'_lt iv hiv
      refine Or.imp_right ?_ ivs'_lt
      exact And.imp_right Nat.le.step
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
no goals