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