[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
n : ℕ
f : α ≃ Fin n
⊢ Nat.card α = n
[PROOFSTEP]
simpa only [card_eq_fintype_card, Fintype.card_fin] using card_congr f
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
cases fintypeOrInfinite α
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Fintype α
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
simpa only [card_eq_fintype_card] using Fintype.equivFin α
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val✝ : Infinite α
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
simp only [card_eq_zero_of_infinite, ne_eq] at h 
[GOAL]
α : Type u_1
β : Type u_2
a : α
inst✝ : Subsingleton α
⊢ Nat.card α = 1
[PROOFSTEP]
letI := Fintype.ofSubsingleton a
[GOAL]
α : Type u_1
β : Type u_2
a : α
inst✝ : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Nat.card α = 1
[PROOFSTEP]
rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : IsEmpty α
⊢ Nat.card α = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
have := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
have := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
simp_rw [Nat.card_eq_fintype_card, Fintype.card_sum]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
⊢ Nat.card (α × β) = Nat.card α * Nat.card β
[PROOFSTEP]
simp only [Nat.card, mk_prod, toNat_mul, toNat_lift]
[GOAL]
α : Type u_1
β✝ : Type u_2
β : α → Type u_3
inst✝ : Fintype α
⊢ Nat.card ((a : α) → β a) = ∏ a : α, Nat.card (β a)
[PROOFSTEP]
simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, toNat_finset_prod]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Finite α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
[PROOFSTEP]
rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
⊢ Nat.card (ZMod n) = n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
⊢ Nat.card (ZMod zero) = zero
[PROOFSTEP]
exact @Nat.card_eq_zero_of_infinite _ Int.infinite
[GOAL]
case succ
α : Type u_1
β : Type u_2
n✝ : ℕ
⊢ Nat.card (ZMod (succ n✝)) = succ n✝
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, ZMod.card]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
⊢ card (α ⊕ β) = card α + card β
[PROOFSTEP]
simp only [PartENat.card, Cardinal.mk_sum, map_add, Cardinal.toPartENat_lift]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n ≤ ↑toPartENat c ↔ ↑n ≤ c
[PROOFSTEP]
rw [← toPartENat_cast n, toPartENat_le_iff_of_le_aleph0 (le_of_lt (nat_lt_aleph0 n))]
[GOAL]
α : Type u_1
β : Type u_2
c : Cardinal.{u_3}
n : ℕ
⊢ ↑toPartENat c ≤ ↑n ↔ c ≤ ↑n
[PROOFSTEP]
rw [← toPartENat_cast n, toPartENat_le_iff_of_lt_aleph0 (nat_lt_aleph0 n)]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n = ↑toPartENat c ↔ ↑n = c
[PROOFSTEP]
rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toPartENat_le_natCast_iff, Cardinal.natCast_le_toPartENat_iff]
[GOAL]
α : Type u_1
β : Type u_2
c : Cardinal.{u_3}
n : ℕ
⊢ ↑toPartENat c = ↑n ↔ c = ↑n
[PROOFSTEP]
rw [eq_comm, Cardinal.natCast_eq_toPartENat_iff, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n < ↑toPartENat c ↔ ↑n < c
[PROOFSTEP]
simp only [← not_le, Cardinal.toPartENat_le_natCast_iff]
[GOAL]
α : Type u_1
β : Type u_2
n : ℕ
c : Cardinal.{u_3}
⊢ ↑toPartENat c < ↑n ↔ c < ↑n
[PROOFSTEP]
simp only [← not_le, Cardinal.natCast_le_toPartENat_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α = 0 ↔ IsEmpty α
[PROOFSTEP]
rw [← Cardinal.mk_eq_zero_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α = 0 ↔ #α = 0
[PROOFSTEP]
conv_rhs => rw [← Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α = 0
[PROOFSTEP]
rw [← Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α = 0
[PROOFSTEP]
rw [← Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α = 0
[PROOFSTEP]
rw [← Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α = 0 ↔ #α = ↑0
[PROOFSTEP]
simp only [← Cardinal.toPartENat_eq_natCast_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α = 0 ↔ ↑toPartENat #α = ↑0
[PROOFSTEP]
simp only [PartENat.card, Nat.cast_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α ≤ 1 ↔ Subsingleton α
[PROOFSTEP]
rw [← le_one_iff_subsingleton]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α ≤ 1 ↔ #α ≤ 1
[PROOFSTEP]
conv_rhs => rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α ≤ 1
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α ≤ 1
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| #α ≤ 1
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α ≤ 1 ↔ #α ≤ ↑1
[PROOFSTEP]
rw [← Cardinal.toPartENat_le_natCast_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ card α ≤ 1 ↔ ↑toPartENat #α ≤ ↑1
[PROOFSTEP]
simp only [PartENat.card, Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ 1 < card α ↔ Nontrivial α
[PROOFSTEP]
rw [← Cardinal.one_lt_iff_nontrivial]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ 1 < card α ↔ 1 < #α
[PROOFSTEP]
conv_rhs => rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| 1 < #α
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| 1 < #α
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
| 1 < #α
[PROOFSTEP]
rw [← Nat.cast_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ 1 < card α ↔ ↑1 < #α
[PROOFSTEP]
rw [← natCast_lt_toPartENat_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ 1 < card α ↔ ↑1 < ↑toPartENat #α
[PROOFSTEP]
simp only [PartENat.card, Nat.cast_one]
