case a
α : Type u
n : ℕ
⊢ map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
α : Type u
n : ℕ
⊢ finRange (Nat.succ n) = 0 :: map Fin.succ (finRange n)
apply map_injective_iff.mpr Fin.val_injective
case a
α : Type u
n : ℕ
⊢ 0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map (Fin.val ∘ Fin.succ) (finRange n)
case a
α : Type u
n : ℕ
⊢ map Fin.val (finRange (Nat.succ n)) = map Fin.val (0 :: map Fin.succ (finRange n))
rw [map_cons, map_coe_finRange, range_succ_eq_map, Fin.val_zero, ← map_coe_finRange, map_map,
  map_map]
no goals
case a
α : Type u
n : ℕ
⊢ 0 :: map (Nat.succ ∘ Fin.val) (finRange n) = 0 :: map (Fin.val ∘ Fin.succ) (finRange n)
simp only [Function.comp, Fin.val_succ]