exact ⟨Nat.le_trans fi ij, jl⟩
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 : ∀ (k : Fin n), first ≤ ↑k → ↑k ≤ last → first ≤ ↑(p.to_map k) ∧ ↑(p.to_map k) ≤ last
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
k' : Fin n := if k = i then j else if k = j then i else k
ki : k = i
x✝ : Decidable (k = j)
⊢ first ≤ ↑j ∧ ↑j ≤ last
no goals