let ⟨f', ⟨h1, h2⟩⟩ := ih
case step
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
⊢ invertible (permuted.step i j fi ij jl p).to_map
case step
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
⊢ invertible (permuted.step i j fi ij jl p).to_map