. exact fun iv => ⟨⟨iv.1,iv.2⟩, iv.3, iv.4⟩
case refine_1
n : Nat
x : Permutation n
⊢ Inversion x → { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }

case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }), ∃ a, ?refine_1 a = b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x), ?refine_1 a₁ = ?refine_1 a₂ → a₁ = a₂
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }),
    ∃ a,
      { val := (a.fst, a.snd),
          property :=
            (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
        b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂