case a
α : Type ?u.8321
β : Type ?u.8324
n : ℕ
i : Fin n
⊢ map valEmbedding (Iio (↑castSucc i)) = map valEmbedding (map castSucc.toEmbedding (Iio i))
α : Type ?u.8321
β : Type ?u.8324
n : ℕ
i : Fin n
⊢ Iio (↑castSucc i) = map castSucc.toEmbedding (Iio i)
apply Finset.map_injective Fin.valEmbedding
case a
α : Type ?u.8321
β : Type ?u.8324
n : ℕ
i : Fin n
⊢ Iio ↑(↑castSucc i) = map (Function.Embedding.trans castSucc.toEmbedding valEmbedding) (Iio i)
case a
α : Type ?u.8321
β : Type ?u.8324
n : ℕ
i : Fin n
⊢ map valEmbedding (Iio (↑castSucc i)) = map valEmbedding (map castSucc.toEmbedding (Iio i))
rw [Finset.map_map, Fin.map_valEmbedding_Iio]
no goals
case a
α : Type ?u.8321
β : Type ?u.8324
n : ℕ
i : Fin n
⊢ Iio ↑(↑castSucc i) = map (Function.Embedding.trans castSucc.toEmbedding valEmbedding) (Iio i)
exact (Fin.map_valEmbedding_Iio i).symm