case a
α : Type ?u.6717
β : Type ?u.6720
n : ℕ
⊢ map valEmbedding (Iio (last n)) = map valEmbedding (map castSucc.toEmbedding univ)
α : Type ?u.6717
β : Type ?u.6720
n : ℕ
⊢ Iio (last n) = map castSucc.toEmbedding univ
apply Finset.map_injective Fin.valEmbedding
case a
α : Type ?u.6717
β : Type ?u.6720
n : ℕ
⊢ Iio n = map (Function.Embedding.trans castSucc.toEmbedding valEmbedding) univ
case a
α : Type ?u.6717
β : Type ?u.6720
n : ℕ
⊢ map valEmbedding (Iio (last n)) = map valEmbedding (map castSucc.toEmbedding univ)
rw [Finset.map_map, Fin.map_valEmbedding_Iio, Fin.val_last]
no goals
case a
α : Type ?u.6717
β : Type ?u.6720
n : ℕ
⊢ Iio n = map (Function.Embedding.trans castSucc.toEmbedding valEmbedding) univ
exact map_valEmbedding_univ.symm