[GOAL]
a b : ℕ+
⊢ card (Icc a b) = ↑b + 1 - ↑a
[PROOFSTEP]
rw [← Nat.card_Icc]
  -- porting note: I had to change this to `erw` *and* provide the proof, yuck.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
a b : ℕ+
⊢ card (Icc a b) = card (Icc ↑a ↑b)
[PROOFSTEP]
erw [← Finset.map_subtype_embedding_Icc _ a b (fun c x _ hx _ hc _ => hc.trans_le hx)]
[GOAL]
a b : ℕ+
⊢ card (Icc a b) = card (map (Embedding.subtype fun n => 0 < n) (Icc a b))
[PROOFSTEP]
rw [card_map]
[GOAL]
a b : ℕ+
⊢ card (Ico a b) = ↑b - ↑a
[PROOFSTEP]
rw [← Nat.card_Ico]
  -- porting note: I had to change this to `erw` *and* provide the proof, yuck.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
a b : ℕ+
⊢ card (Ico a b) = card (Ico ↑a ↑b)
[PROOFSTEP]
erw [← Finset.map_subtype_embedding_Ico _ a b (fun c x _ hx _ hc _ => hc.trans_le hx)]
[GOAL]
a b : ℕ+
⊢ card (Ico a b) = card (map (Embedding.subtype fun n => 0 < n) (Ico a b))
[PROOFSTEP]
rw [card_map]
[GOAL]
a b : ℕ+
⊢ card (Ioc a b) = ↑b - ↑a
[PROOFSTEP]
rw [← Nat.card_Ioc]
  -- porting note: I had to change this to `erw` *and* provide the proof, yuck.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
a b : ℕ+
⊢ card (Ioc a b) = card (Ioc ↑a ↑b)
[PROOFSTEP]
erw [← Finset.map_subtype_embedding_Ioc _ a b (fun c x _ hx _ hc _ => hc.trans_le hx)]
[GOAL]
a b : ℕ+
⊢ card (Ioc a b) = card (map (Embedding.subtype fun n => 0 < n) (Ioc a b))
[PROOFSTEP]
rw [card_map]
[GOAL]
a b : ℕ+
⊢ card (Ioo a b) = ↑b - ↑a - 1
[PROOFSTEP]
rw [← Nat.card_Ioo]
  -- porting note: I had to change this to `erw` *and* provide the proof, yuck.
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
a b : ℕ+
⊢ card (Ioo a b) = card (Ioo ↑a ↑b)
[PROOFSTEP]
erw [← Finset.map_subtype_embedding_Ioo _ a b (fun c x _ hx _ hc _ => hc.trans_le hx)]
[GOAL]
a b : ℕ+
⊢ card (Ioo a b) = card (map (Embedding.subtype fun n => 0 < n) (Ioo a b))
[PROOFSTEP]
rw [card_map]
[GOAL]
a b : ℕ+
⊢ card (uIcc a b) = Int.natAbs (↑↑b - ↑↑a) + 1
[PROOFSTEP]
rw [← Nat.card_uIcc, ← map_subtype_embedding_uIcc, card_map]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
[PROOFSTEP]
rw [← card_Icc, Fintype.card_ofFinset]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
[PROOFSTEP]
rw [← card_Ico, Fintype.card_ofFinset]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
[PROOFSTEP]
rw [← card_Ioc, Fintype.card_ofFinset]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
[PROOFSTEP]
rw [← card_Ioo, Fintype.card_ofFinset]
[GOAL]
a b : ℕ+
⊢ Fintype.card ↑(Set.uIcc a b) = Int.natAbs (↑↑b - ↑↑a) + 1
[PROOFSTEP]
rw [← card_uIcc, Fintype.card_ofFinset]
