simp [nfyi, fyj, permuted.to_map, f]
case isFalse.isTrue
n first last : Nat
α✝ : Type
arr1 arr2 arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
nfyi : ¬f' y = i
fyj : f' y = j
⊢ f (if f' y = i then j else if f' y = j then i else f' y) = y
case isFalse.isTrue
n first last : Nat
α✝ : Type
arr1 arr2 arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : invertible p.to_map
f' : Fin n → Fin n
h1 : ∀ (x : Fin n), f' (p.to_map x) = x
h2 : ∀ (y : Fin n), p.to_map (f' y) = y
f : Fin n → Fin n := (permuted.step i j fi ij jl p).to_map
g : Fin n → Fin n :=
  fun k =>
    let k' := f' k;
    if k' = i then j else if k' = j then i else k'
gf : ∀ (x : Fin n), g (f x) = x
y : Fin n
nfyi : ¬f' y = i
fyj : f' y = j
⊢ p.to_map j = y