a b : ℤ
⊢ card (map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (toNat (b - a)))) = toNat (b - a)
a b : ℤ
⊢ card (Ico a b) = toNat (b - a)
change (Finset.map _ _).card = _
no goals
a b : ℤ
⊢ card (map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (range (toNat (b - a)))) = toNat (b - a)
rw [Finset.card_map, Finset.card_range]