awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
h : Injective f
this : Fintype β
have : ∀ (this : Fintype α), Surjective f ↔ Nat.card α = Nat.card β
⊢ Surjective f ↔ Nat.card α = Nat.card β

Tactic:
have := Fintype.ofInjective f h
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
h : Injective f
this_1 : Fintype β
this : Fintype α
revert : ∀ (h : Injective f), Surjective f ↔ Nat.card α = Nat.card β
⊢ Surjective f ↔ Nat.card α = Nat.card β

Tactic:
revert h
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
this_1 : Fintype β
this : Fintype α
rw : Injective f ∧ Surjective f ↔ Injective f ∧ Nat.card α = Nat.card β
rw₁ : Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β
rw₂ : Bijective f ↔ Injective f ∧ Fintype.card α = Nat.card β
rw₃ : Bijective f ↔ Injective f ∧ Fintype.card α = Fintype.card β
rw₄ rw₅ : Injective f ∧ Fintype.card α = Fintype.card β ↔ Injective f ∧ Fintype.card α = Fintype.card β
⊢ ∀ (h : Injective f), Surjective f ↔ Nat.card α = Nat.card β

Tactic:
rw [← and_congr_right_iff, ← Bijective,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_injective_and_card]

Premises used: and_congr_right_iff, Fintype.bijective_iff_injective_and_card, Function.Bijective, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
rw : Surjective f → (Injective f ↔ Nat.card α = Nat.card β)
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Tactic:
rw [_root_.and_comm, Bijective, and_congr_left_iff]

Premises used: and_comm, and_congr_left_iff, Function.Bijective
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
h : Surjective f
have : ∀ (this : Fintype α), Injective f ↔ Nat.card α = Nat.card β
⊢ Injective f ↔ Nat.card α = Nat.card β

Tactic:
have := Fintype.ofFinite α
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
h : Surjective f
this : Fintype α
have : ∀ (this : Fintype β), Injective f ↔ Nat.card α = Nat.card β
⊢ Injective f ↔ Nat.card α = Nat.card β

Tactic:
have := Fintype.ofSurjective f h
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
h : Surjective f
this_1 : Fintype α
this : Fintype β
revert : ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
⊢ Injective f ↔ Nat.card α = Nat.card β

Tactic:
revert h
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
this_1 : Fintype α
this : Fintype β
rw : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₂ : Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β
rw₃ : Bijective f ↔ Surjective f ∧ Fintype.card α = Nat.card β
rw₄ : Bijective f ↔ Surjective f ∧ Fintype.card α = Fintype.card β
rw₅ rw₆ : Surjective f ∧ Fintype.card α = Fintype.card β ↔ Surjective f ∧ Fintype.card α = Fintype.card β
⊢ ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β

Tactic:
rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]

Premises used: Fintype.bijective_iff_surjective_and_card, and_comm, and_congr_left_iff, Function.Bijective, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
rw : Bijective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₁ : Injective f ∧ Surjective f ↔ Nat.card α = Nat.card β ∧ Surjective f
rw₂ rw₃ rw₄ rw₅ : ∀ (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
rw₆ : ∀ (h : Surjective f) (this : Fintype α), Injective f ↔ Nat.card α = Nat.card β
rw₇ : ∀ (h : Surjective f) (this : Fintype α) (this : Fintype β), Injective f ↔ Nat.card α = Nat.card β
rw₈ : ∀ (this : Fintype α) (this : Fintype β) (h : Surjective f), Injective f ↔ Nat.card α = Nat.card β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Tactic:
classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]

Premises used: Fintype.bijective_iff_surjective_and_card, and_comm, and_congr_left_iff, Function.Bijective, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite β
f : α → β
inj : Injective f
hc : Nat.card β ≤ Nat.card α
⊢ Bijective f

Tactic:
(Nat.bijective_iff_injective_and_card f).mpr
    ⟨inj, hc.antisymm (card_le_card_of_injective f inj) |>.symm⟩

Premises used: Iff.mpr, Nat.card_le_card_of_injective, LE.le.antisymm, Nat.bijective_iff_injective_and_card, And.intro, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
f : α → β
surj : Surjective f
hc : Nat.card α ≤ Nat.card β
⊢ Bijective f

Tactic:
(Nat.bijective_iff_surjective_and_card f).mpr
    ⟨surj, hc.antisymm (card_le_card_of_surjective f surj)⟩

Premises used: Iff.mpr, Nat.card_le_card_of_surjective, LE.le.antisymm, Nat.bijective_iff_surjective_and_card, And.intro
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
n : ℕ
f : α ≃ Fin n
⊢ Nat.card α = n

Tactic:
simpa only [card_eq_fintype_card, Fintype.card_fin] using card_congr f

Premises used: Fintype.card_fin, Nat.card_congr, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
n : ℕ
rw : Fintype.card (Fin n) = n
rw₁ rw₂ : n = n
⊢ Nat.card (Fin n) = n

Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_fin]

Premises used: Fintype.card_fin, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
h : s ⊆ t
⊢ Nat.card.{u_1} (↑s : Type u_1) ≤ Nat.card.{u_1} (↑t : Type u_1)

Tactic:
toNat_le_toNat (mk_le_mk_of_subset h) ht.lt_aleph0

Premises used: Nat.card, Cardinal.toNat_le_toNat, Cardinal.mk_le_mk_of_subset, Set.Finite.lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) ≤ Nat.card.{u_1} (↑s : Type u_1)

Tactic:
have := hs.to_subtype
  card_le_card_of_surjective (imageFactorization f s) imageFactorization_surjective

Premises used: Nat.card_le_card_of_surjective, Set.imageFactorization, Set.Finite.to_subtype, Set.imageFactorization_surjective
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
inl : ∀ (hs : s.Finite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
inr : ∀ (hs : s.Infinite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
obtain hs | hs := s.finite_or_infinite

Premises used: Set.finite_or_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
inl : ∀ (this : Fintype (↑s : Type u_1)), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
have := hs.fintype
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
this : Fintype (↑s : Type u_1)
inl : Fintype.card.{u_2} (↑(f '' s) : Type u_2) = Fintype.card.{u_1} (↑s : Type u_1)
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]

Premises used: Set.card_image_of_inj_on, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
⊢ Infinite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have := hs.to_subtype
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
⊢ Infinite.{u_2 + 1} (↑(f '' s) : Type u_2)

Tactic:
have := (hs.image hf).to_subtype
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
this_1 : Infinite.{u_1 + 1} (↑s : Type u_1)
this : Infinite.{u_2 + 1} (↑(f '' s) : Type u_2)
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
simp [Nat.card_eq_zero_of_infinite]

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
inl : ∀ (hs : s.Finite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
inr inr₁ : ∀ (hs : s.Infinite), Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
classical
  obtain hs | hs := s.finite_or_infinite
  · have := hs.fintype
    simp_rw [Nat.card_eq_fintype_card, Set.card_image_of_inj_on hf]
  · have := hs.to_subtype
    have := (hs.image hf).to_subtype
    simp [Nat.card_eq_zero_of_infinite]

Premises used: Set.finite_or_infinite, Nat.card_eq_zero_of_infinite, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ Nat.card.{u_2} (↑(f '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
card_image_of_injOn hf.injOn

Premises used: Function.Injective.injOn, Nat.card_image_of_injOn
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
e : α ≃ β
⊢ Nat.card.{u_2} (↑((⇑e : (a : α) → β) '' s) : Type u_2) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
Nat.card_congr (e.image s).symm

Premises used: Nat.card_congr, Equiv.image, Equiv.symm
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
rw : Nat.card.{u_2} (↑(f '' f ⁻¹' s) : Type u_2) = Nat.card.{u_2} (↑s : Type u_2)
rw₁ rw₂ : Nat.card.{u_2} (↑s : Type u_2) = Nat.card.{u_2} (↑s : Type u_2)
⊢ Nat.card.{u_1} (↑(f ⁻¹' s) : Type u_1) = Nat.card.{u_2} (↑s : Type u_2)

Tactic:
rw [← Nat.card_image_of_injOn hf, image_preimage_eq_iff.2 hsf]

Premises used: Iff.mpr, Nat.card_image_of_injOn, Set.image_preimage_eq_iff
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Injective f
hsf : s ⊆ range f
⊢ Nat.card.{u_1} (↑(f ⁻¹' s) : Type u_1) = Nat.card.{u_2} (↑s : Type u_2)

Tactic:
card_preimage_of_injOn hf.injOn hsf

Premises used: Function.Injective.injOn, Nat.card_preimage_of_injOn
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ Nat.card.{u_1} (↑univ : Type u_1) = Nat.card α

Tactic:
card_congr (Equiv.Set.univ α)

Premises used: Nat.card_congr, Equiv.Set.univ
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
rw : Nat.card.{u_1} (↑(f ⁻¹' range f) : Type u_1) = Nat.card α
⊢ Nat.card.{u_2} (↑(range f) : Type u_2) = Nat.card α

Tactic:
rw [← Nat.card_preimage_of_injective hf le_rfl]

Premises used: le_rfl, Nat.card_preimage_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card.{u_1} (↑(f ⁻¹' range f) : Type u_1) = Nat.card α

Tactic:
simp [Nat.card_univ]

Premises used: Nat.card_univ
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
inl : Fintype α → α ≃ Fin (Nat.card α)
inr : Infinite α → α ≃ Fin (Nat.card α)
⊢ α ≃ Fin (Nat.card α)

Tactic:
cases fintypeOrInfinite α

Premises used: fintypeOrInfinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val : Fintype α
⊢ α ≃ Fin (Nat.card α)

Tactic:
simpa only [card_eq_fintype_card] using Fintype.equivFin α

Premises used: Fintype.equivFin, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
val : Infinite α
⊢ α ≃ Fin (Nat.card α)

Tactic:
simp only [card_eq_zero_of_infinite, ne_eq, not_true_eq_false] at h

Premises used: Nat.card_eq_zero_of_infinite, not_true_eq_false, ne_eq
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
a : α
inst : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
rw : Fintype.card α = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ Nat.card α = 1

Tactic:
rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]

Premises used: Fintype.card_ofSubsingleton, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ Nat.card α = 1 ↔ Subsingleton α ∧ Nonempty α

Tactic:
Cardinal.toNat_eq_one_iff_unique

Premises used: Nat.card, Cardinal.toNat_eq_one_iff_unique
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Nonempty α
inst_1 : Subsingleton α
⊢ Nat.card α = 1

Tactic:
simp [card_eq_one_iff_unique, *]

Premises used: Nat.card_eq_one_iff_unique
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
rw : Subsingleton α ∧ Nonempty α ↔ ∃ (x : α), ∀ (y : α), y = x
⊢ Nat.card α = 1 ↔ ∃ (x : α), ∀ (y : α), y = x

Tactic:
rw [card_eq_one_iff_unique]

Premises used: Nat.card_eq_one_iff_unique
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ Subsingleton α ∧ Nonempty α ↔ ∃ (x : α), ∀ (y : α), y = x

Tactic:
⟨fun ⟨s, ⟨a⟩⟩ ↦ ⟨a, fun x ↦ s.elim x a⟩, fun ⟨x, h⟩ ↦ ⟨subsingleton_of_forall_eq x h, ⟨x⟩⟩⟩

Premises used: subsingleton_of_forall_eq, _private.0.Nat.card_eq_one_iff_exists.match_2, Exists, Nonempty.intro, And, And.intro, Iff.intro, Exists.intro, Nonempty, Subsingleton, Subsingleton.elim, _private.0.Nat.card_eq_one_iff_exists.match_1
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ Subsingleton α ∧ Nonempty α ↔ ∃ (x : α), ∀ (y : α), y = x

Tactic:
exact ⟨fun ⟨s, ⟨a⟩⟩ ↦ ⟨a, fun x ↦ s.elim x a⟩, fun ⟨x, h⟩ ↦ ⟨subsingleton_of_forall_eq x h, ⟨x⟩⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ Nat.card α = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ Eq (α := Set α) {x, y} Set.univ

Tactic:
toNat_eq_ofNat.trans mk_eq_two_iff

Premises used: Nat.card, Cardinal.mk_eq_two_iff, Iff.trans, Cardinal.toNat_eq_ofNat
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
x : α
⊢ Nat.card α = 2 ↔ ∃! y : α, y ≠ x

Tactic:
toNat_eq_ofNat.trans (mk_eq_two_iff' x)

Premises used: Cardinal.mk_eq_two_iff', Nat.card, Iff.trans, Cardinal.toNat_eq_ofNat
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ Nat.card.{u_1} { _a : α // True } = Nat.card α

Tactic:
card_congr <| Equiv.subtypeUnivEquiv fun _ => trivial

Premises used: trivial, Equiv.subtypeUnivEquiv, Nat.card_congr
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
have : ∀ (this : Fintype α), Nat.card (α ⊕ β) = Nat.card α + Nat.card β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
have := Fintype.ofFinite α
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this : Fintype α
have : ∀ (this : Fintype β), Nat.card (α ⊕ β) = Nat.card α + Nat.card β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
have := Fintype.ofFinite β
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this_1 : Fintype α
this : Fintype β
simp_rw : Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Tactic:
simp_rw [Nat.card_eq_fintype_card, Fintype.card_sum]

Premises used: Nat.card_eq_fintype_card, Fintype.card_sum
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
⊢ Nat.card (α × β) = Nat.card α * Nat.card β

Tactic:
simp only [Nat.card, mk_prod, toNat_mul, toNat_lift]

Premises used: Cardinal.toNat_mul, Nat.card, Cardinal.toNat_lift, Cardinal.mk_prod
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ Nat.card (ULift.{u_4, u_3} α) = Nat.card α

Tactic:
card_congr Equiv.ulift

Premises used: Equiv.ulift, Nat.card_congr
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ Nat.card.{u_3 + 1} (PLift α) = Nat.card α

Tactic:
card_congr Equiv.plift

Premises used: Nat.card_congr, Equiv.plift
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : α → Type u_3
inst : Fintype α
inst_1 : ∀ (a : α), Finite.{u_3 + 1} (β a)
x : (a : α) → Fintype (β a) := fun (a : α) ↦ Fintype.ofFinite (β a)
simp_rw : Fintype.card (Sigma β) = ∑ x_1 : α, Fintype.card.{u_3} (β x_1)
⊢ Nat.card (Sigma β) = ∑ a : α, Nat.card.{u_3} (β a)

Tactic:
simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma]

Premises used: Fintype.card_sigma, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : α → Type u_3
inst : Fintype α
simp_rw :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) #((a : α) → β a) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
simp_rw₁ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) (prod.{u_1, u_3} fun (i : α) ↦ #(β i)) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
simp_rw₂ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) (lift.{u_1, u_3} (∏ i : α, #(β i))) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
simp_rw₃ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{u_3}) → ℕ) (∏ i : α, #(β i)) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
⊢ Nat.card ((a : α) → β a) = ∏ a : α, Nat.card.{u_3} (β a)

Tactic:
simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, _root_.map_prod]

Premises used: Cardinal.mk_pi, Nat.card, Cardinal.toNat_lift, map_prod, Cardinal.prod_eq_of_fintype
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
haveI : ∀ (this : Fintype α), Nat.card (α → β) = Nat.card β ^ Nat.card α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
this : Fintype α
rw : ∏ a : α, Nat.card β = Nat.card β ^ Nat.card α
rw₁ : Nat.card β ^ Finset.card.{u_1} (α := α) Finset.univ = Nat.card β ^ Nat.card α
rw₂ : Nat.card β ^ Fintype.card α = Nat.card β ^ Nat.card α
rw₃ rw₄ : Nat.card β ^ Nat.card α = Nat.card β ^ Nat.card α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α

Tactic:
rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]

Premises used: Finset.card_univ, Finset.prod_const, Nat.card_pi, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
n : ℕ
zero : Nat.card (ZMod 0) = 0
succ : ∀ (n : ℕ), Nat.card (ZMod (n + 1)) = n + 1
⊢ Nat.card (ZMod n) = n

Tactic:
cases n
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
⊢ Nat.card (ZMod 0) = 0

Tactic:
@Nat.card_eq_zero_of_infinite _ Int.infinite

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
⊢ Nat.card (ZMod 0) = 0

Tactic:
exact @Nat.card_eq_zero_of_infinite _ Int.infinite

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
n : ℕ
succ : Fintype.card (ZMod (n + 1)) = n + 1
succ₁ succ₂ : n + 1 = n + 1
⊢ Nat.card (ZMod (n + 1)) = n + 1

Tactic:
rw [Nat.card_eq_fintype_card, ZMod.card]

Premises used: ZMod.card, Nat.card_eq_fintype_card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
a : α
t : Set β
rw : Nat.card (↑(Prod.mk a '' t) : Type (max u_2 u_1)) = Nat.card.{u_2} (↑t : Type u_2)
rw₁ rw₂ : Nat.card.{u_2} (↑t : Type u_2) = Nat.card.{u_2} (↑t : Type u_2)
⊢ Nat.card (↑(SProd.sprod (α := Set α) {a} t) : Type (max u_2 u_1)) = Nat.card.{u_2} (↑t : Type u_2)

Tactic:
rw [singleton_prod, Nat.card_image_of_injective (Prod.mk_right_injective a)]

Premises used: Nat.card_image_of_injective, Set.singleton_prod, Prod.mk_right_injective
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
b : β
rw : Nat.card (↑((fun (a : α) ↦ (a, b)) '' s) : Type (max u_1 u_2)) = Nat.card.{u_1} (↑s : Type u_1)
rw₁ rw₂ : Nat.card.{u_1} (↑s : Type u_1) = Nat.card.{u_1} (↑s : Type u_1)
⊢ Nat.card (↑(SProd.sprod (β := Set β) s {b}) : Type (max u_1 u_2)) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
rw [prod_singleton, Nat.card_image_of_injective (Prod.mk_left_injective b)]

Premises used: Nat.card_image_of_injective, Set.prod_singleton, Prod.mk_left_injective
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 0 < Nat.card.{u_1} (↑s : Type u_1) ↔ s.Nonempty

Tactic:
simp [pos_iff_ne_zero, Nat.card_eq_zero, hs.to_subtype, nonempty_iff_ne_empty]

Premises used: Set.Finite.to_subtype, Set.nonempty_iff_ne_empty, pos_iff_ne_zero, Nat.card_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
rw : Nat.card.{u_1} (↑(Prod.fst '' graphOn f s) : Type u_1) = Nat.card.{u_1} (↑s : Type u_1)
rw₁ rw₂ : Nat.card.{u_1} (↑s : Type u_1) = Nat.card.{u_1} (↑s : Type u_1)
⊢ Nat.card (↑(graphOn f s) : Type (max u_1 u_2)) = Nat.card.{u_1} (↑s : Type u_1)

Tactic:
rw [← Nat.card_image_of_injOn fst_injOn_graph, image_fst_graphOn]

Premises used: Set.fst_injOn_graph, Nat.card_image_of_injOn, Set.image_fst_graphOn
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Fintype α
⊢ card α = (↑(Fintype.card α) : ℕ∞)

Tactic:
simp [card]

Premises used: ENat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Infinite α
⊢ card α = ⊤

Tactic:
simp only [card, toENat_eq_top, aleph0_le_mk]

Premises used: Cardinal.toENat_eq_top, ENat.card, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ card α = ⊤ ↔ Infinite α

Tactic:
simp [card, aleph0_le_mk_iff]

Premises used: Cardinal.aleph0_le_mk_iff, ENat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Finite α
⊢ card α < ⊤

Tactic:
simp [card]

Premises used: ENat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ card α < ⊤ ↔ Finite α

Tactic:
simp [card, lt_aleph0_iff_finite]

Premises used: Cardinal.lt_aleph0_iff_finite, ENat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
⊢ card (α ⊕ β) = card α + card β

Tactic:
simp only [card, mk_sum, map_add, toENat_lift]

Premises used: Cardinal.toENat_lift, map_add, Cardinal.mk_sum, ENat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
f : α ≃ β
⊢ card α = card β

Tactic:
Cardinal.toENat_congr f

Premises used: ENat.card, Cardinal.toENat_congr
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ card (ULift.{u_4, u_3} α) = card α

Tactic:
card_congr Equiv.ulift

Premises used: ENat.card_congr, Equiv.ulift
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ card.{u_3 + 1} (PLift α) = card α

Tactic:
card_congr Equiv.plift

Premises used: ENat.card_congr, Equiv.plift
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
f : α → β
s : Set α
h : Set.InjOn f s
⊢ card.{u_4} (↑(f '' s) : Type u_4) = card.{u_3} (↑s : Type u_3)

Tactic:
card_congr (Equiv.Set.imageOfInjOn f s h).symm

Premises used: ENat.card_congr, Equiv.Set.imageOfInjOn, Equiv.symm
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
f : α → β
s : Set α
h : Injective f
⊢ card.{u_4} (↑(f '' s) : Type u_4) = card.{u_3} (↑s : Type u_3)

Tactic:
card_image_of_injOn h.injOn

Premises used: ENat.card_image_of_injOn, Function.Injective.injOn
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
rw : card (ULift.{u_4, u_3} α) ≤ card (ULift.{u_3, u_4} β)
⊢ card α ≤ card β

Tactic:
rw [← card_ulift α, ← card_ulift β]

Premises used: ENat.card_ulift
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ card (ULift.{u_4, u_3} α) ≤ card (ULift.{u_3, u_4} β)

Tactic:
Cardinal.gciENat.gc.monotone_u <| Cardinal.lift_mk_le_lift_mk_of_injective hf

Premises used: GaloisConnection.monotone_u, Cardinal.gciENat, GaloisCoinsertion.gc, Cardinal.lift_mk_le_lift_mk_of_injective, ENat.card