α : Type u
n : ℕ
⊢ map (fun a => a) (range n) = range n
α : Type u
n : ℕ
⊢ map Fin.val (finRange n) = range n
simp_rw [finRange, map_pmap, pmap_eq_map]
no goals
α : Type u
n : ℕ
⊢ map (fun a => a) (range n) = range n
exact List.map_id _