induction p with
| refl => simp [permuted.to_map, invertible_id]
| step i j fi ij jl p ih =>
  let ⟨f', ⟨h1, h2⟩⟩ := ih
  let f := permuted.to_map (permuted.step i j fi ij jl p)
  show invertible f
  let g := fun (k : Fin n) =>
    let k' := f' k
    if k' = i then j
    else if k' = j then i
    else k'
  have gf : ∀x, g (f x) = x := by
    intro x
    simp (config := {zeta := false}) [f, permuted.to_map]
    cases decEq x i with
    | isFalse nxi =>
      cases decEq x j with
      | isFalse nxj => simp [nxi, nxj, g, h1]
      | isTrue xj => simp [nxi, xj, g, h1]
    | isTrue xi => simp [xi, g, h1]
  have fg : ∀y, f (g y) = y := by
    intro y
    simp (config := {zeta := false}) [g]
    show f (if f' y = i then j else if f' y = j then i else f' y) = y
    cases decEq (f' y) i with
    | isFalse nfyi =>
      cases decEq (f' y) j with
      | isFalse nfyj => simp [nfyi, nfyj, permuted.to_map, h2, f]
      | isTrue fyj =>
        simp [nfyi, fyj, permuted.to_map, f]
        rw [←(congrArg p.to_map fyj), h2]
    | isTrue fyi =>
      simp [fyi, f, permuted.to_map]
      have : (if j = i then j else i) = i := by simp
      rw [this, ←(congrArg p.to_map fyi), h2]
  exact ⟨g, ⟨gf, fg⟩⟩
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
⊢ invertible p.to_map
no goals