[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
have := (Finite.exists_equiv_fin α).choose_spec.some
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
this : α ≃ Fin (Exists.choose (_ : ∃ n, Nonempty (α ≃ Fin n)))
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
rwa [Nat.card_eq_of_equiv_fin this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
n : ℕ
h : Nat.card α = n
⊢ α ≃ Fin n
[PROOFSTEP]
subst h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ α ≃ Fin (Nat.card α)
[PROOFSTEP]
apply Finite.equivFin
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
[PROOFSTEP]
cases finite_or_infinite α
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
h✝ : Finite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
[PROOFSTEP]
letI := Fintype.ofFinite α
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
h✝ : Finite α
this : Fintype α := Fintype.ofFinite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
[PROOFSTEP]
simp only [*, Nat.card_eq_fintype_card, dif_pos]
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
h✝ : Infinite α
⊢ Nat.card α = if h : Finite α then Fintype.card α else 0
[PROOFSTEP]
simp only [*, card_eq_zero_of_infinite, not_finite_iff_infinite.mpr, dite_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ 0 < Nat.card α ↔ Nonempty α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ 0 < Nat.card α ↔ Nonempty α
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_le_one_iff_subsingleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ 1 < Nat.card α ↔ Nontrivial α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ 1 < Nat.card α ↔ Nontrivial α
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.one_lt_card_iff_nontrivial]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ Nat.card (Option α) = Nat.card α + 1
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Option α) = Nat.card α + 1
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_option]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite β
f : α → β
hf : Function.Injective f
⊢ Nat.card α ≤ Nat.card β
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite β
f : α → β
hf : Function.Injective f
this : Fintype β
⊢ Nat.card α ≤ Nat.card β
[PROOFSTEP]
haveI := Fintype.ofInjective f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite β
f : α → β
hf : Function.Injective f
this✝ : Fintype β
this : Fintype α
⊢ Nat.card α ≤ Nat.card β
[PROOFSTEP]
simpa only [Nat.card_eq_fintype_card, ge_iff_le] using Fintype.card_le_of_injective f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
⊢ Nat.card β ≤ Nat.card α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this : Fintype α
⊢ Nat.card β ≤ Nat.card α
[PROOFSTEP]
haveI := Fintype.ofSurjective f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
f : α → β
hf : Function.Surjective f
this✝ : Fintype α
this : Fintype β
⊢ Nat.card β ≤ Nat.card α
[PROOFSTEP]
simpa only [Nat.card_eq_fintype_card, ge_iff_le] using Fintype.card_le_of_surjective f hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
⊢ Nat.card α = 0 ↔ IsEmpty α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = 0 ↔ IsEmpty α
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
⊢ Nat.card α = 0
[PROOFSTEP]
cases finite_or_infinite β
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
⊢ Nat.card α = 0
[PROOFSTEP]
haveI := card_eq_zero_iff.mp h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this : IsEmpty β
⊢ Nat.card α = 0
[PROOFSTEP]
haveI := Function.isEmpty f
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Finite β
this✝ : IsEmpty β
this : IsEmpty α
⊢ Nat.card α = 0
[PROOFSTEP]
exact Nat.card_of_isEmpty
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
⊢ Nat.card α = 0
[PROOFSTEP]
haveI := Infinite.of_surjective f hf
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h✝ : Infinite β
this : Infinite α
⊢ Nat.card α = 0
[PROOFSTEP]
exact Nat.card_eq_zero_of_infinite
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
haveI := Fintype.ofFinite β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Fintype.card_sum]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
p : α → Prop
⊢ Nat.card { x // p x } ≤ Nat.card α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
p : α → Prop
this : Fintype α
⊢ Nat.card { x // p x } ≤ Nat.card α
[PROOFSTEP]
simpa only [Nat.card_eq_fintype_card, ge_iff_le] using Fintype.card_subtype_le p
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
⊢ Nat.card { x // p x } < Nat.card α
[PROOFSTEP]
haveI := Fintype.ofFinite α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card { x // p x } < Nat.card α
[PROOFSTEP]
simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ card α = ↑(Nat.card α)
[PROOFSTEP]
unfold PartENat.card
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ ↑Cardinal.toPartENat (Cardinal.mk α) = ↑(Nat.card α)
[PROOFSTEP]
apply symm
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = ↑Cardinal.toPartENat (Cardinal.mk α)
[PROOFSTEP]
rw [Cardinal.natCast_eq_toPartENat_iff]
[GOAL]
case a
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.mk α
[PROOFSTEP]
exact Finite.cast_card_eq_mk
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
cases' _root_.finite_or_infinite (↥(s ∪ t)) with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h 
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
h : Finite ↑s ∧ Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
cases h
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
rw [← Cardinal.natCast_le, Nat.cast_add, Finite.cast_card_eq_mk, Finite.cast_card_eq_mk, Finite.cast_card_eq_mk]
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
left✝ : Finite ↑s
right✝ : Finite ↑t
⊢ Cardinal.mk ↑(s ∪ t) ≤ Cardinal.mk ↑s + Cardinal.mk ↑t
[PROOFSTEP]
exact Cardinal.mk_union_le s t
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Set α
h : Infinite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
[PROOFSTEP]
exact Nat.card_eq_zero_of_infinite.trans_le (zero_le _)
