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', ⟨index, fk', kl'⟩⟩ := ih k fk kl
  let k'' := if k' = i then j else if k' = j then i else k'
  exists k''
  have : (if k'' = i then j else if k'' = j then i else k'') = k' := by
    match decEq k' i, decEq k' j with
    | isTrue ki, _ => simp [k'', ki]
    | _, isTrue kj => simp [k'', kj]
    | isFalse ki, isFalse kj => simp [k'',ki, kj]
  rw [this]
  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 ⟨index, 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
⊢ ∃ k', p.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
no goals