awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
n : ℕ
c : Cardinal.{u_3}
rw :
  LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) (↑n : Cardinal.{u_3}) : ℕ∞)
      ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔
    (↑n : Cardinal.{u_3}) ≤ c
rw₁ rw₂ : (↑n : Cardinal.{u_3}) ≤ c ↔ (↑n : Cardinal.{u_3}) ≤ c
⊢ LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u_3}) ≤ c

Tactic:
rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 natCast_le_aleph0]

Premises used: Cardinal.toENat_le_iff_of_le_aleph0, Cardinal.toENat_nat, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
c : Cardinal.{u_3}
n : ℕ
⊢ LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔ c ≤ (↑n : Cardinal.{u_3})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
n : ℕ
c : Cardinal.{u_3}
rw :
  LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧
      LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔
    (↑n : Cardinal.{u_3}) = c
rw₁ :
  LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧
      LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔
    (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3})
rw₂ :
  LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧ c ≤ (↑n : Cardinal.{u_3}) ↔
    (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3})
rw₃ rw₄ : (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3}) ↔ (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3})
⊢ Eq (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u_3}) = c

Tactic:
rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toENat_le_natCast, Cardinal.natCast_le_toENat]

Premises used: Cardinal.natCast_le_toENat, Cardinal.toENat_le_natCast, le_antisymm_iff
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
c : Cardinal.{u_3}
n : ℕ
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔ c = (↑n : Cardinal.{u_3})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
n : ℕ
c : Cardinal.{u_3}
⊢ LT.lt (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u_3}) < c

Tactic:
simp only [← not_le, Cardinal.toENat_le_natCast]

Premises used: not_le, Cardinal.toENat_le_natCast
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
n : ℕ
c : Cardinal.{u_3}
⊢ LT.lt (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔ c < (↑n : Cardinal.{u_3})

Tactic:
simp only [← not_le, Cardinal.natCast_le_toENat]

Premises used: not_le, Cardinal.natCast_le_toENat
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
rw : card α = 0 ↔ #α = 0
⊢ card α = 0 ↔ IsEmpty α

Tactic:
rw [← Cardinal.mk_eq_zero_iff]

Premises used: Cardinal.mk_eq_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ card α = 0 ↔ #α = 0

Tactic:
simp [card]

Premises used: ENat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ card α ≠ 0 ↔ Nonempty α

Tactic:
simp [card_eq_zero_iff_empty]

Premises used: ENat.card_eq_zero_iff_empty
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ 1 ≤ card α ↔ Nonempty α

Tactic:
simp [one_le_iff_ne_zero, card_eq_zero_iff_empty]

Premises used: ENat.card_eq_zero_iff_empty, ENat.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Nonempty α
⊢ 0 < card α

Tactic:
simpa [pos_iff_ne_zero, card_ne_zero_iff_nonempty]

Premises used: ENat.card_ne_zero_iff_nonempty, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
⊢ 0 < card α ↔ Nonempty α

Tactic:
simp [pos_iff_ne_zero, card_ne_zero_iff_nonempty]

Premises used: ENat.card_ne_zero_iff_nonempty, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
rw : card α ≤ 1 ↔ #α ≤ 1
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
rw [← le_one_iff_subsingleton]

Premises used: Cardinal.le_one_iff_subsingleton
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ card α ≤ 1 ↔ #α ≤ 1

Tactic:
simp [card]

Premises used: ENat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Subsingleton α
⊢ card α ≤ 1

Tactic:
simpa [card_le_one_iff_subsingleton]

Premises used: ENat.card_le_one_iff_subsingleton
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
rw : card α ≤ 1 ∧ 1 ≤ card α ↔ Subsingleton α ∧ Nonempty α
⊢ card α = 1 ↔ Nonempty.{max 1 (u_3 + 1)} (Unique α)

Tactic:
rw [unique_iff_subsingleton_and_nonempty α, le_antisymm_iff]

Premises used: unique_iff_subsingleton_and_nonempty, le_antisymm_iff
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ card α ≤ 1 ∧ 1 ≤ card α ↔ Subsingleton α ∧ Nonempty α

Tactic:
and_congr (card_le_one_iff_subsingleton α) (one_le_card_iff_nonempty α)

Premises used: ENat.one_le_card_iff_nonempty, ENat.card_le_one_iff_subsingleton, and_congr
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ card α ≤ 1 ∧ 1 ≤ card α ↔ Subsingleton α ∧ Nonempty α

Tactic:
exact and_congr (card_le_one_iff_subsingleton α) (one_le_card_iff_nonempty α)

Premises used: ENat.one_le_card_iff_nonempty, ENat.card_le_one_iff_subsingleton, and_congr
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
rw : 1 < card α ↔ 1 < #α
⊢ 1 < card α ↔ Nontrivial α

Tactic:
rw [← Cardinal.one_lt_iff_nontrivial]

Premises used: Cardinal.one_lt_iff_nontrivial
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
rw : 1 < card α ↔ LT.lt (α := ℕ∞) ((↑1 : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) #α : ℕ∞)
⊢ 1 < card α ↔ (↑1 : Cardinal.{u_3}) < #α

Tactic:
rw [← natCast_lt_toENat]

Premises used: Cardinal.natCast_lt_toENat
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
⊢ 1 < card α ↔ LT.lt (α := ℕ∞) ((↑1 : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) #α : ℕ∞)

Tactic:
simp only [ENat.card, Nat.cast_one]

Premises used: ENat.card, Nat.cast_one
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
inst : Nontrivial α
⊢ 1 < card α

Tactic:
simpa [one_lt_card_iff_nontrivial]

Premises used: ENat.one_lt_card_iff_nontrivial
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_1
h : 3 ≤ card α
x y : α
⊢ 3 ≤ #α

Tactic:
simpa [ENat.card] using h

Premises used: ENat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
⊢ card (α × β) = card α * card β

Tactic:
simp [ENat.card]

Premises used: ENat.card
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
inl : ∀ (α_emp : IsEmpty α), card (α → β) = card β ^ card α
inr : ∀ (α_emp : Nonempty α), card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α

Tactic:
rcases isEmpty_or_nonempty α with α_emp | α_emp

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : IsEmpty α
⊢ card (α → β) = card β ^ card α

Tactic:
simp [(card_eq_zero_iff_empty α).2 α_emp]

Premises used: Iff.mpr, ENat.card_eq_zero_iff_empty
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
inr : Finite α → card (α → β) = card β ^ card α
inr₁ : Infinite α → card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α

Tactic:
rcases finite_or_infinite α

Premises used: finite_or_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Finite α
inr : Finite β → card (α → β) = card β ^ card α
inr₁ : Infinite β → card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α

Tactic:
rcases finite_or_infinite β

Premises used: finite_or_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Finite α
h_1 : Finite β
this_1 : Fintype α := Fintype.ofFinite α
this : Fintype β := Fintype.ofFinite β
⊢ card (α → β) = card β ^ card α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Finite α
h_1 : Infinite β
inr : ⊤ = HPow.hPow (α := ℕ∞) ⊤ (card α)
⊢ card (α → β) = card β ^ card α

Tactic:
simp only [card_eq_top_of_infinite]

Premises used: ENat.card_eq_top_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Finite α
h_1 : Infinite β
⊢ ⊤ = HPow.hPow (α := ℕ∞) ⊤ (card α)

Tactic:
(top_epow (one_le_iff_ne_zero.1 ((one_le_card_iff_nonempty α).2 α_emp))).symm

Premises used: Iff.mpr, ENat.one_le_card_iff_nonempty, ENat.top_epow, Iff.mp, Eq.symm, ENat.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Finite α
h_1 : Infinite β
⊢ ⊤ = HPow.hPow (α := ℕ∞) ⊤ (card α)

Tactic:
exact (top_epow (one_le_iff_ne_zero.1 ((one_le_card_iff_nonempty α).2 α_emp))).symm

Premises used: Iff.mpr, ENat.one_le_card_iff_nonempty, ENat.top_epow, Iff.mp, Eq.symm, ENat.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
inr : card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
⊢ card (α → β) = card β ^ card α

Tactic:
rw [card_eq_top_of_infinite (α := α)]

Premises used: ENat.card_eq_top_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
inr : ∀ (b_0 : card β < 1), card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
inr₁ : ∀ (b_1 : card β = 1), card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
inr₂ : ∀ (b_2 : 1 < card β), card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤

Tactic:
rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2

Premises used: OfNat.ofNat, ENat.card, lt_trichotomy
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_0 : card β < 1
⊢ IsEmpty β

Tactic:
rw [lt_one_iff_eq_zero, card_eq_zero_iff_empty] at b_0

Premises used: ENat.card_eq_zero_iff_empty, ENat.lt_one_iff_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_0 : IsEmpty β
inr : IsEmpty (α → β)
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤

Tactic:
rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]

Premises used: Iff.mpr, ENat.card_eq_zero_iff_empty, ENat.zero_epow_top
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_0 : IsEmpty β
⊢ IsEmpty (α → β)

Tactic:
simp [b_0]
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_1 : card β = 1
inr : card (α → β) = 1
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤

Tactic:
rw [b_1, one_epow]

Premises used: ENat.one_epow
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_1 : card β = 1
inr : card (α → β) ≤ 1
inr₁ : 1 ≤ card (α → β)
⊢ card (α → β) = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_1 : card β = 1
this : Subsingleton β := ⋯
⊢ card (α → β) ≤ 1

Tactic:
(card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton

Premises used: Iff.mpr, ENat.card_le_one_iff_subsingleton, Pi.instSubsingleton
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_1 : card β = 1
this : Subsingleton β := ⋯
⊢ card (α → β) ≤ 1

Tactic:
exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton

Premises used: Iff.mpr, ENat.card_le_one_iff_subsingleton, Pi.instSubsingleton
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_1 : card β = 1
this : Nonempty β := ⋯
⊢ 1 ≤ card (α → β)

Tactic:
(one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty

Premises used: Iff.mpr, ENat.one_le_card_iff_nonempty, Pi.instNonempty
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_1 : card β = 1
this : Nonempty β := ⋯
⊢ 1 ≤ card (α → β)

Tactic:
exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty

Premises used: Iff.mpr, ENat.one_le_card_iff_nonempty, Pi.instNonempty
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_2 : 1 < card β
inr : Infinite (α → β)
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤

Tactic:
rw [epow_top b_2, card_eq_top]

Premises used: ENat.card_eq_top, ENat.epow_top
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_2 : 1 < card β
⊢ Nontrivial β

Tactic:
rw [one_lt_card_iff_nontrivial β] at b_2

Premises used: ENat.one_lt_card_iff_nontrivial
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_2 : Nontrivial β
⊢ Infinite (α → β)

Tactic:
Pi.infinite_of_left

Premises used: Pi.infinite_of_left
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_2 : Nontrivial β
⊢ Infinite (α → β)

Tactic:
exact Pi.infinite_of_left

Premises used: Pi.infinite_of_left
-- Module: Mathlib.SetTheory.Cardinal.Finite
Goal:
α : Type u_3
β : Type u_4
inl : ∀ (α_emp : IsEmpty α), card (α → β) = card β ^ card α
inr inr₁ : ∀ (α_emp : Nonempty α), card (α → β) = card β ^ card α
inr₂ : ∀ (α_emp : Nonempty α), Finite α → card (α → β) = card β ^ card α
inr₃ inr₄ : ∀ (α_emp : Nonempty α), Infinite α → card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α

Tactic:
classical
  rcases isEmpty_or_nonempty α with α_emp | α_emp
  · simp [(card_eq_zero_iff_empty α).2 α_emp]
  rcases finite_or_infinite α
  · rcases finite_or_infinite β
    · letI := Fintype.ofFinite α
      letI := Fintype.ofFinite β
      simp
    · simp only [card_eq_top_of_infinite]
      exact (top_epow (one_le_iff_ne_zero.1 ((one_le_card_iff_nonempty α).2 α_emp))).symm
  · rw [card_eq_top_of_infinite (α := α)]
    rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
    · rw [lt_one_iff_eq_zero, card_eq_zero_iff_empty] at b_0
      rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
      simp [b_0]
    · rw [b_1, one_epow]
      apply le_antisymm
      · letI := (card_le_one_iff_subsingleton β).1 b_1.le
        exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton
      · letI := (one_le_card_iff_nonempty β).1 b_1.ge
        exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty
    · rw [epow_top b_2, card_eq_top]
      rw [one_lt_card_iff_nontrivial β] at b_2
      exact Pi.infinite_of_left

Premises used: ENat.one_lt_card_iff_nontrivial, ENat.card_eq_zero_iff_empty, finite_or_infinite, isEmpty_or_nonempty, ENat.card_eq_top, ENat.card_eq_top_of_infinite, le_antisymm, Pi.infinite_of_left, OfNat.ofNat, ENat.card, ENat.zero_epow_top, lt_trichotomy, ENat.lt_one_iff_eq_zero, ENat.one_epow
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Fintype α
inst_1 : Zero β
⊢ #(α →₀ β) = lift.{u, v} #β ^ Fintype.card α

Tactic:
simpa using (@Finsupp.equivFunOnFinite α β _ _).cardinal_eq

Premises used: Finsupp.equivFunOnFinite, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α β : Type u
inst : Fintype α
inst_1 : Zero β
⊢ #(α →₀ β) = #β ^ Fintype.card α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
a : #(α →₀ β) ≤ max (lift.{v, u} #α) (lift.{u, v} #β)
a₁ : max (lift.{v, u} #α) (lift.{u, v} #β) ≤ #(α →₀ β)
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ #(α →₀ β) ≤ #(Finset (α × β))

Tactic:
mk_le_of_injective (Finsupp.graph_injective α β)

Premises used: Cardinal.mk_le_of_injective, Finsupp.graph_injective
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ #(Finset (α × β)) = #(α × β)

Tactic:
mk_finset_of_infinite _

Premises used: Cardinal.mk_finset_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
h : ℵ₀ ≤ lift.{v, u} #α
h' : lift.{u, v} #β ≠ 0
⊢ #(α × β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
rw [mk_prod, mul_eq_max_of_aleph0_le_left]

Premises used: Cardinal.mul_eq_max_of_aleph0_le_left, Cardinal.mk_prod
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ ℵ₀ ≤ lift.{v, u} #α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ lift.{u, v} #β ≠ 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
mk_le_of_injective : #(α × β) = max (lift.{v, u} #α) (lift.{u, v} #β)
⊢ #(α →₀ β) ≤ max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
calc
      #(α →₀ β) ≤ #(Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
      _ = #(α × β) := mk_finset_of_infinite _
      _ = max (lift.{v} #α) (lift.{u} #β) := by
        rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp

Premises used: Finset, Cardinal.mk_finset_of_infinite, Cardinal.mk_le_of_injective, Prod, Finsupp.graph_injective, Finsupp
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
a : lift.{v, u} #α ≤ #(α →₀ β)
a₁ : lift.{u, v} #β ≤ #(α →₀ β)
⊢ max (lift.{v, u} #α) (lift.{u, v} #β) ≤ #(α →₀ β)

Tactic:
apply max_le

Premises used: max_le
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
a : lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)
⊢ lift.{v, u} #α ≤ #(α →₀ β)

Tactic:
rw [← lift_id #(α →₀ β), ← lift_umax]

Premises used: Cardinal.mk, Cardinal.lift_umax, Finsupp, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
a : lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)
⊢ lift.{u, v} #β ≤ #(α →₀ β)

Tactic:
rw [← lift_id #(α →₀ β), ← lift_umax]

Premises used: Cardinal.mk, Cardinal.lift_umax, Finsupp, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
a : ∀ (b : β) (hb : b ≠ 0), lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
obtain ⟨b, hb⟩ := exists_ne (0 : β)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
b : β
hb : b ≠ 0
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩

Premises used: Iff.mpr, Cardinal.lift_mk_le, Function.Embedding.mk, Finsupp.single_left_injective, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
b : β
hb : b ≠ 0
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
a : ∀ (inhabited_h : Inhabited α), lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
inhabit α
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
inhabited_h : Inhabited α
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩

Premises used: Iff.mpr, Finsupp.single_injective, Cardinal.lift_mk_le, Inhabited.default, Function.Embedding.mk, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
inhabited_h : Inhabited α
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α β : Type u
inst : Infinite α
inst_1 : Zero β
inst_2 : Nontrivial β
⊢ #(α →₀ β) = max #α #β

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
inl : ∀ (val : Fintype α), #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
inr : Infinite α → #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
cases fintypeOrInfinite α

Premises used: fintypeOrInfinite
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
inl : lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
rw [mk_finsupp_lift_of_fintype]

Premises used: Cardinal.mk_finsupp_lift_of_fintype
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
⊢ ℵ₀ ≤ lift.{u, v} #β

Tactic:
have : ℵ₀ ≤ (#β).lift := aleph0_le_lift.2 (aleph0_le_mk β)
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
inl : 1 ≤ Fintype.card α
rw : lift.{v, u} #α ≤ ℵ₀
⊢ lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
rw [max_eq_right (le_trans _ this), power_nat_eq this]

Premises used: Cardinal.power_nat_eq, max_eq_right, le_trans
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ 1 ≤ Fintype.card α

Tactic:
Fintype.card_pos

Premises used: Fintype.card_pos, Nat.lt
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ lift.{v, u} #α ≤ ℵ₀

Tactic:
lift_le_aleph0.2 (lt_aleph0_of_finite _).le

Premises used: Iff.mpr, Cardinal.lift_le_aleph0, LT.lt.le, Cardinal.lt_aleph0_of_finite
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Fintype α
this : ℵ₀ ≤ lift.{u, v} #β
⊢ 1 ≤ Fintype.card α

Tactic:
exacts [Fintype.card_pos, lift_le_aleph0.2 (lt_aleph0_of_finite _).le]

Premises used: Iff.mpr, Cardinal.lift_le_aleph0, LT.lt.le, Cardinal.lt_aleph0_of_finite, Fintype.card_pos
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
β : Type v
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
val : Infinite α
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
apply mk_finsupp_lift_of_infinite

Premises used: Cardinal.mk_finsupp_lift_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α β : Type u
inst : Nonempty α
inst_1 : Zero β
inst_2 : Infinite β
⊢ #(α →₀ β) = max #α #β

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
inst : Nonempty α
⊢ #(α →₀ ℕ) = max #α ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Finsupp
Goal:
α : Type u
inst : IsEmpty α
⊢ #(α →₀ ℕ) = 1

Tactic:
simp