n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (↑σ) (finRange n) ↔ a ∈ finRange n
n : ℕ
σ : Perm (Fin n)
⊢ map (↑σ) (finRange n) ~ finRange n
rw [perm_ext ((nodup_finRange n).map σ.injective) <| nodup_finRange n]
no goals
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (↑σ) (finRange n) ↔ a ∈ finRange n
simpa [mem_map, mem_finRange, true_and_iff, iff_true_iff] using σ.surjective