induction p generalizing k with
| refl => simp [permuted.to_map, fk, kl]
| step i j fi ij jl p ih =>
  simp [permuted.to_map]
  let k' := if k = i then j else if k = j then i else k
  have : first ≤ k'.val ∧ k'.val ≤ last := by
    match decEq k i, decEq k j with
    | isTrue ki, _ =>
      simp [k', ki]
      exact ⟨Nat.le_trans fi ij, jl⟩
    | isFalse ki, isTrue kj =>
      simp [k', ki]
      simp [kj]
      exact ⟨fi, Nat.le_trans ij jl⟩
    | isFalse ki, isFalse kj =>
      simp [k', ki, kj]
      exact ⟨fk, kl⟩
  exact ih k' this.1 this.2
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
no goals