. intro k hk invs IH hjk
  have : i.1 < k := trans (r:=LT.lt (α:=Nat)) hlt (Nat.le_of_succ_le_succ hjk)
  refine Nat.fold'_induction (motive := fun l (ivs' : Array (Inversion x)) => (i.1 < l ∨ j.1 < k) → ⟨i,j,hlt,hinv⟩ ∈ ivs') k _ invs ?_ ?_ (Or.inl this)
  all_goals simp
  . intro hi
    cases hi with
    | inl hi => cases hi
    | inr hj => exact IH hj
  . intro l hl invs' IH' hil
    cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hjk) with
    | inl heq =>
      cases heq
      have : i.1 ≤ l :=
        Nat.le_of_succ_le_succ (Or.resolve_right hil j.1.lt_irrefl)
      cases Nat.eq_or_lt_of_le this with
      | inl heq =>
        cases heq; rewrite [dif_pos hinv]
        exact Array.mem_push.mpr <| Or.inr rfl
      | inr hlt =>
        specialize IH' (Or.inl hlt)
        if hx : x[l]'(Nat.lt_trans hl j.2) > x[j.1] then
          rewrite [dif_pos hx]
          exact Array.mem_push.mpr <| Or.inl IH'
        else
          rewrite [dif_neg hx]; exact IH'
    | inr hlt =>
      specialize IH' (Or.inr hlt)
      if hx : x[l]'(Nat.lt_trans hl hk) > x[k]'hk then
        rewrite [dif_pos hx]
        exact Array.mem_push.mpr <| Or.inl IH'
      else
        rewrite [dif_neg hx]; exact IH'
case succ
n : Nat
x : Permutation n
iv : Inversion x
i j : Fin n
hlt : i < j
hinv : x[↑i] > x[↑j]
⊢ ∀ (i_1 : Nat) (hi : i_1 < n) (a : Array (Inversion x)),
    (↑j < i_1 → { fst := i, snd := j, lt := hlt, inverted := hinv } ∈ a) →
      ↑j < i_1 + 1 →
        { fst := i, snd := j, lt := hlt, inverted := hinv } ∈
          Nat.fold' i_1
            (fun i ivs =>
              if h : x[↑i] > x[i_1] then
                Array.push ivs
                  { fst := Fin.castLE (_ : ↑{ val := i_1, isLt := hi } ≤ n) i, snd := { val := i_1, isLt := hi },
                    lt := (_ : ↑i < ↑{ val := i_1, isLt := hi }), inverted := h }
              else ivs)
            a
no goals