awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Uncountable α
⊢ ℵ₀ < #α

Tactic:
aleph0_lt_mk_iff.mpr ‹_›

Premises used: Iff.mpr, Cardinal.aleph0_lt_mk_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
⊢ CanLift Cardinal.{u_1} ℕ Nat.cast fun (x : Cardinal.{u_1}) ↦ x < ℵ₀

Tactic:
⟨fun _ hx =>
    let ⟨n, hn⟩ := lt_aleph0.mp hx
    ⟨n, hn.symm⟩⟩

Premises used: Exists, _private.0.Cardinal.lt_aleph0.match_1, Nat.cast, Exists.intro, Iff.mp, Cardinal.lt_aleph0, CanLift.mk, Eq.symm, Eq
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
m n : ℕ
ha : (↑m : Cardinal.{u_1}) < ℵ₀
hb : (↑n : Cardinal.{u_1}) < ℵ₀
rw : (↑(m + n) : Cardinal.{u_1}) < ℵ₀
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) < ℵ₀

Tactic:
rw [← Nat.cast_add]

Premises used: Nat.cast_add
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
m n : ℕ
ha : (↑m : Cardinal.{u_1}) < ℵ₀
hb : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ (↑(m + n) : Cardinal.{u_1}) < ℵ₀

Tactic:
apply natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
⊢ a + b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀

Tactic:
⟨fun h => ⟨(self_le_add_right _ _).trans_lt h, (self_le_add_left _ _).trans_lt h⟩,
   fun ⟨h1, h2⟩ => add_lt_aleph0 h1 h2⟩

Premises used: self_le_add_right, self_le_add_left, _private.0.Cardinal.add_lt_aleph0_iff.match_1, Cardinal.aleph0, HAdd.hAdd, And.intro, LT.lt, Iff.intro, LE.le.trans_lt, Cardinal.add_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a + b ↔ ℵ₀ ≤ a ∨ ℵ₀ ≤ b

Tactic:
simp only [← not_lt, add_lt_aleph0_iff, not_and_or]

Premises used: Cardinal.add_lt_aleph0_iff, not_lt, not_and_or
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ HSMul.hSMul (α := ℕ) 0 a < ℵ₀ ↔ Eq (α := ℕ) 0 0 ∨ a < ℵ₀

Tactic:
simpa using aleph0_pos

Premises used: Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ HSMul.hSMul (α := ℕ) 1 a < ℵ₀ ↔ Eq (α := ℕ) 1 0 ∨ a < ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
n : ℕ
rw : (n + 1 = 0 ∨ a < ℵ₀) ∧ a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀
⊢ (n + 2) • a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀

Tactic:
rw [succ_nsmul, add_lt_aleph0_iff, nsmul_lt_aleph0_iff]

Premises used: Cardinal.add_lt_aleph0_iff, succ_nsmul
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
n : ℕ
⊢ (n + 1 = 0 ∨ a < ℵ₀) ∧ a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
a : Cardinal.{u_1}
h : n ≠ 0
⊢ n • a < ℵ₀ ↔ a < ℵ₀

Tactic:
nsmul_lt_aleph0_iff.trans <| or_iff_right h

Premises used: Cardinal.nsmul_lt_aleph0_iff, or_iff_right, Iff.trans
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
m n : ℕ
ha : (↑m : Cardinal.{u_1}) < ℵ₀
hb : (↑n : Cardinal.{u_1}) < ℵ₀
rw : (↑(m * n) : Cardinal.{u_1}) < ℵ₀
⊢ HMul.hMul (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) < ℵ₀

Tactic:
rw [← Nat.cast_mul]

Premises used: Nat.cast_mul
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
m n : ℕ
ha : (↑m : Cardinal.{u_1}) < ℵ₀
hb : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ (↑(m * n) : Cardinal.{u_1}) < ℵ₀

Tactic:
apply natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
⊢ a * b < ℵ₀ ↔ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
refine_1 : ∀ (h : a * b < ℵ₀), a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
refine_2 : a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀
⊢ a * b < ℵ₀ ↔ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
pos : ∀ (ha : a = 0), a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
neg : ∀ (ha : ¬a = 0), a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
exact Or.inl ha

Premises used: Or.inl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
neg : b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
right
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
pos : ∀ (hb : b = 0), b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
neg : ∀ (hb : ¬b = 0), b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
by_cases hb : b = 0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
Or.inl hb

Premises used: Or.inl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
exact Or.inl hb

Premises used: Or.inl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
neg : a < ℵ₀ ∧ b < ℵ₀
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
right
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ 1 ≤ a

Tactic:
rw [← Ne, ← Cardinal.one_le_iff_ne_zero] at ha hb

Premises used: Cardinal.one_le_iff_ne_zero, Ne
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
ha₁ : 1 ≤ a
⊢ 1 ≤ b

Tactic:
rw [← Ne, ← Cardinal.one_le_iff_ne_zero] at ha hb

Premises used: Cardinal.one_le_iff_ne_zero, Ne
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
neg : a < ℵ₀
neg₁ : b < ℵ₀
⊢ a < ℵ₀ ∧ b < ℵ₀

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
neg : a * 1 < ℵ₀
⊢ a < ℵ₀

Tactic:
rw [← mul_one a]

Premises used: mul_one
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a * 1 < ℵ₀

Tactic:
(mul_le_mul' le_rfl hb).trans_lt h

Premises used: le_rfl, LE.le.trans_lt, mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a * 1 < ℵ₀

Tactic:
exact (mul_le_mul' le_rfl hb).trans_lt h

Premises used: le_rfl, LE.le.trans_lt, mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
neg : 1 * b < ℵ₀
⊢ b < ℵ₀

Tactic:
rw [← one_mul b]

Premises used: one_mul
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 * b < ℵ₀

Tactic:
(mul_le_mul' ha le_rfl).trans_lt h

Premises used: le_rfl, LE.le.trans_lt, mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 * b < ℵ₀

Tactic:
exact (mul_le_mul' ha le_rfl).trans_lt h

Premises used: le_rfl, LE.le.trans_lt, mul_le_mul'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
b : Cardinal.{u_1}
⊢ 0 * b < ℵ₀

Tactic:
simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Cardinal.mul_lt_aleph0, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a : Cardinal.{u_1}
⊢ a * 0 < ℵ₀

Tactic:
simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Cardinal.mul_lt_aleph0, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b < ℵ₀

Tactic:
simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Cardinal.mul_lt_aleph0, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
h : ¬a * b < ℵ₀ ↔ ¬(a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀) := ⋯
rwa : ∀ (h : ℵ₀ ≤ a * b ↔ ¬(a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀)), ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
rwa₁ : ∀ (h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬(b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀)), ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
rwa₂ : ∀ (h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ ¬(a < ℵ₀ ∧ b < ℵ₀)), ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
rwa₃ : ∀ (h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ (¬a < ℵ₀ ∨ ¬b < ℵ₀)), ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
rwa₄ : ∀ (h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ (ℵ₀ ≤ a ∨ ¬b < ℵ₀)), ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)), ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Tactic:
rwa [not_lt, not_or, not_or, not_and_or, not_lt, not_lt] at h

Premises used: not_or, not_lt, not_and_or
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u}
⊢ ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0

Tactic:
have : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0 := fun a => ne_bot_of_le_ne_bot aleph0_ne_zero a
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
simp : b ≠ 0 ∧ ℵ₀ ≤ a ∨ a ≠ 0 ∧ ℵ₀ ≤ b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Tactic:
simp only [aleph0_le_mul_iff, and_or_left, and_iff_right_of_imp this, @and_left_comm (a ≠ 0)]

Premises used: and_or_left, and_left_comm, and_iff_right_of_imp, Cardinal.aleph0_le_mul_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
⊢ b ≠ 0 ∧ ℵ₀ ≤ a ∨ a ≠ 0 ∧ ℵ₀ ≤ b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Tactic:
simp only [and_comm, or_comm]

Premises used: and_comm, or_comm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀

Tactic:
simp [mul_lt_aleph0_iff, ha, hb]

Premises used: Cardinal.mul_lt_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
m n : ℕ
ha : (↑m : Cardinal.{u_1}) < ℵ₀
hb : (↑n : Cardinal.{u_1}) < ℵ₀
rw : (↑(m ^ n) : Cardinal.{u_1}) < ℵ₀
⊢ HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) < ℵ₀

Tactic:
rw [power_natCast, ← Nat.cast_pow]

Premises used: Nat.cast_pow, Cardinal.power_natCast
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
a b : Cardinal.{u_1}
m n : ℕ
ha : (↑m : Cardinal.{u_1}) < ℵ₀
hb : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ (↑(m ^ n) : Cardinal.{u_1}) < ℵ₀

Tactic:
apply natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
⊢ #α = 1 ↔ Subsingleton α ∧ Nonempty α

Tactic:
calc
    #α = 1 ↔ #α ≤ 1 ∧ 1 ≤ #α := le_antisymm_iff
    _ ↔ Subsingleton α ∧ Nonempty α :=
      le_one_iff_subsingleton.and (Cardinal.one_le_iff_ne_zero.trans mk_ne_zero_iff)

Premises used: Cardinal.mk_ne_zero_iff, Trans.trans, Cardinal.le_one_iff_subsingleton, Cardinal.one_le_iff_ne_zero, le_antisymm_iff, Iff.and, Iff.trans
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
rw : Infinite α ↔ ¬#α < ℵ₀
rw₁ : Infinite α ↔ ¬Finite α
rw₂ rw₃ : Infinite α ↔ Infinite α
⊢ Infinite α ↔ ℵ₀ ≤ #α

Tactic:
rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]

Premises used: not_finite_iff_infinite, not_lt, Cardinal.lt_aleph0_iff_finite
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ ℵ₀ ≤ #α ↔ Infinite α

Tactic:
infinite_iff.symm

Premises used: Cardinal.infinite_iff, Iff.symm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #α < ℵ₀ ↔ Finite α

Tactic:
simp [← not_le, aleph0_le_mk_iff]

Premises used: not_le, Cardinal.aleph0_le_mk_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Finite α
⊢ #α < ℵ₀

Tactic:
mk_lt_aleph0_iff.2 ‹_›

Premises used: Iff.mpr, Cardinal.mk_lt_aleph0_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Infinite α
⊢ ℵ₀ ≤ #α

Tactic:
infinite_iff.1 ‹_›

Premises used: Cardinal.infinite_iff, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
inst : Infinite α
h : #α ≤ #β
⊢ Infinite β

Tactic:
infinite_iff.2 <| (aleph0_le_mk α).trans h

Premises used: Iff.mpr, Cardinal.infinite_iff, LE.le.trans, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
inst : Countable α
inst_1 : Infinite α
⊢ #α = ℵ₀

Tactic:
mk_le_aleph0.antisymm <| aleph0_le_mk _

Premises used: Cardinal.mk_le_aleph0, LE.le.antisymm, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
h : #α = ℵ₀
obtain : ∀ (f : α ≃ ULift.{u, 0} ℕ), Nonempty.{u + 1} (Denumerable α)
⊢ Nonempty.{u + 1} (Denumerable α)

Tactic:
obtain ⟨f⟩ := Quotient.exact h

Premises used: Quotient.exact
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
h : #α = ℵ₀
f : α ≃ ULift.{u, 0} ℕ
⊢ Nonempty.{u + 1} (Denumerable α)

Tactic:
⟨Denumerable.mk' <| f.trans Equiv.ulift⟩

Premises used: Equiv.trans, Equiv.ulift, Nonempty.intro, Denumerable.mk'
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
h : #α = ℵ₀
f : α ≃ ULift.{u, 0} ℕ
⊢ Nonempty.{u + 1} (Denumerable α)

Tactic:
exact ⟨Denumerable.mk' <| f.trans Equiv.ulift⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Denumerable α
⊢ #α = ℵ₀

Tactic:
denumerable_iff.1 ⟨‹_›⟩

Premises used: Nonempty.intro, Iff.mp, Cardinal.denumerable_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
s : Set α
rw : s.Countable ∧ s.Infinite ↔ Countable.{u_1 + 1} (↑s : Type u_1) ∧ Infinite.{u_1 + 1} (↑s : Type u_1)
rw₁ :
  s.Countable ∧ Infinite.{u_1 + 1} (↑s : Type u_1) ↔
    Countable.{u_1 + 1} (↑s : Type u_1) ∧ Infinite.{u_1 + 1} (↑s : Type u_1)
rw₂ rw₃ : s.Countable ∧ Infinite.{u_1 + 1} (↑s : Type u_1) ↔ s.Countable ∧ Infinite.{u_1 + 1} (↑s : Type u_1)
⊢ s.Countable ∧ s.Infinite ↔ Nonempty.{u_1 + 1} (Denumerable (↑s : Type u_1))

Tactic:
rw [nonempty_denumerable_iff, ← Set.infinite_coe_iff, countable_coe_iff]

Premises used: Set.countable_coe_iff, Set.infinite_coe_iff, nonempty_denumerable_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ ℵ₀ + ℵ₀ = ℵ₀

Tactic:
mk_denumerable _

Premises used: Cardinal.mk, Quotient.map₂, Quotient.mk', Cardinal.map₂, Cardinal.mk_denumerable
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ ℵ₀ * ℵ₀ = ℵ₀

Tactic:
mk_denumerable _

Premises used: Cardinal.mk, Quotient.map₂, Quotient.mk', Cardinal.map₂, Cardinal.mk_denumerable
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
hn : n ≠ 0
rwa : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑1 : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
rwa₁ : 1 ≤ n
rwa₂ rwa₃ rwa₄ rwa₅ : n ≠ 0
⊢ LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑n : Cardinal.{u_1})

Tactic:
rwa [← Nat.cast_one, Nat.cast_le, Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero, Nat.cast_le, Nat.cast_one
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
hn : n ≠ 0
rw : (↑n : Cardinal.{u_1}) * ℵ₀ = ℵ₀
rw₁ rw₂ : ℵ₀ = ℵ₀
⊢ ℵ₀ * (↑n : Cardinal.{u_1}) = ℵ₀

Tactic:
rw [mul_comm, nat_mul_aleph0 hn]

Premises used: Cardinal.nat_mul_aleph0, mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n * ℵ₀ = ℵ₀

Tactic:
nat_mul_aleph0 (NeZero.ne n)

Premises used: Cardinal.nat_mul_aleph0, NeZero.ne
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ ℵ₀ * OfNat.ofNat n = ℵ₀

Tactic:
aleph0_mul_nat (NeZero.ne n)

Premises used: Cardinal.aleph0_mul_nat, NeZero.ne
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c₁ c₂ : Cardinal.{u_1}
⊢ c₁ + c₂ ≤ ℵ₀ ↔ c₁ ≤ ℵ₀ ∧ c₂ ≤ ℵ₀

Tactic:
⟨fun h => ⟨le_self_add.trans h, le_add_self.trans h⟩, fun h =>
    aleph0_add_aleph0 ▸ add_le_add h.1 h.2⟩

Premises used: add_le_add, Eq.rec, Cardinal.aleph0_add_aleph0, And.right, And.left, And.intro, Iff.intro, LE.le.trans, le_self_add, le_add_self
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
⊢ ℵ₀ + (↑n : Cardinal.{u_1}) = ℵ₀

Tactic:
(add_le_aleph0.2 ⟨le_rfl, natCast_le_aleph0⟩).antisymm le_self_add

Premises used: Iff.mpr, Cardinal.add_le_aleph0, le_rfl, LE.le.antisymm, And.intro, le_self_add, Cardinal.natCast_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
rw : ℵ₀ + (↑n : Cardinal.{u_1}) = ℵ₀
rw₁ rw₂ : ℵ₀ = ℵ₀
⊢ (↑n : Cardinal.{u_1}) + ℵ₀ = ℵ₀

Tactic:
rw [add_comm, aleph0_add_nat]

Premises used: Cardinal.aleph0_add_nat, add_comm
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n + ℵ₀ = ℵ₀

Tactic:
nat_add_aleph0 n

Premises used: Cardinal.nat_add_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ ℵ₀ + OfNat.ofNat n = ℵ₀

Tactic:
aleph0_add_nat n

Premises used: Cardinal.aleph0_add_nat
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
n : ℕ
h : c ≤ (↑n : Cardinal.{u_1})
⊢ c < ℵ₀

Tactic:
h.trans_lt natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
c : Cardinal.{u_1}
n : ℕ
h : c ≤ (↑n : Cardinal.{u_1})
lift :
  ∀ (c : ℕ) (h : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑c : Cardinal.{u_1}) (↑n : Cardinal.{u_1})),
    ∃ m ≤ n, Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑c : Cardinal.{u_1}) (↑m : Cardinal.{u_1})
⊢ ∃ m ≤ n, c = (↑m : Cardinal.{u_1})

Tactic:
lift c to ℕ using h.trans_lt natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n c : ℕ
h : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑c : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
⊢ ∃ m ≤ n, Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑c : Cardinal.{u_1}) (↑m : Cardinal.{u_1})

Tactic:
⟨c, mod_cast h, rfl⟩

Premises used: cast, Nat.cast_le._simp_1, And.intro, Exists.intro, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
n c : ℕ
h : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑c : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
⊢ ∃ m ≤ n, Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑c : Cardinal.{u_1}) (↑m : Cardinal.{u_1})

Tactic:
exact ⟨c, mod_cast h, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ #ℤ = ℵ₀

Tactic:
mk_denumerable ℤ

Premises used: Int, Cardinal.mk_denumerable
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
⊢ #ℕ+ = ℵ₀

Tactic:
mk_denumerable ℕ+

Premises used: Cardinal.mk_denumerable, PNat
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #(Additive α) = #α

Tactic:
rfl

Premises used: Additive, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #(Multiplicative α) = #α

Tactic:
rfl

Premises used: Multiplicative, rfl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #αᵐᵒᵖ = #α

Tactic:
mk_congr MulOpposite.opEquiv.symm

Premises used: MulOpposite.opEquiv, Equiv.symm, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
x : α
⊢ #(↑{x} : Type u) = 1

Tactic:
mk_eq_one _

Premises used: Cardinal.mk_eq_one
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
n : ℕ
⊢ #(Fin n → α) = #α ^ n

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #((n : ℕ) × List.Vector α n) = sum fun (n : ℕ) ↦ #α ^ n

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
rw : (sum fun (n : ℕ) ↦ #PEmpty.{u_1 + 1} ^ n) = 1
rw₁ : #(List PEmpty.{u_1 + 1}) = 1
rw₂ rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) 1 1
⊢ (sum fun (n : ℕ) ↦ HPow.hPow (α := Cardinal.{u_1}) 0 n) = 1

Tactic:
rw [← mk_eq_zero (α := PEmpty), ← mk_list_eq_sum_pow, mk_eq_one]

Premises used: Cardinal.mk_eq_zero, Cardinal.mk_list_eq_sum_pow, PEmpty, Cardinal.mk_eq_one
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
r : α → α → Prop
⊢ #(Quot r) ≤ #α

Tactic:
mk_le_of_surjective Quot.exists_rep

Premises used: Cardinal.mk_le_of_surjective, Quot.exists_rep
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Setoid α
⊢ #(Quotient s) ≤ #α

Tactic:
mk_quot_le

Premises used: Cardinal.mk_quot_le, Quotient
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
p q : α → Prop
h : ∀ ⦃x : α⦄, p x → q x
⊢ #(Subtype p) ≤ #(Subtype q)

Tactic:
⟨Embedding.subtypeMap (Embedding.refl α) h⟩

Premises used: Nonempty.intro, Function.Embedding.subtypeMap, Function.Embedding.refl
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ #(↑s : Type u_1) ≤ #(↑t : Type u_1)

Tactic:
⟨Set.embeddingOfSubset s t h⟩

Premises used: Nonempty.intro, Set.embeddingOfSubset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ Monotone (α := Set α) (mk ∘ Elem)

Tactic:
fun _ _ ↦ mk_le_mk_of_subset

Premises used: Monotone, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #(↑∅ : Type u) = 0

Tactic:
mk_eq_zero _

Premises used: Cardinal.mk_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
rw : IsEmpty.{u + 1} (↑s : Type u) ↔ s = ∅
rw₁ rw₂ : s = ∅ ↔ s = ∅
⊢ #(↑s : Type u) = 0 ↔ s = ∅

Tactic:
rw [mk_eq_zero_iff, isEmpty_coe_sort]

Premises used: Set.isEmpty_coe_sort, Cardinal.mk_eq_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
rw : Nonempty.{u + 1} (↑s : Type u) ↔ s.Nonempty
rw₁ rw₂ : s.Nonempty ↔ s.Nonempty
⊢ #(↑s : Type u) ≠ 0 ↔ s.Nonempty

Tactic:
rw [mk_ne_zero_iff, nonempty_coe_sort]

Premises used: Cardinal.mk_ne_zero_iff, Set.nonempty_coe_sort
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
⊢ #(↑univ : Type u) = #α

Tactic:
mk_congr (Equiv.Set.univ α)

Premises used: Cardinal.mk_congr, Equiv.Set.univ
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
s : Set α
t : Set β
rw : #(↑(s ×ˢ t) : Type u) = #((↑s : Type u) × (↑t : Type u))
rw₁ rw₂ : #((↑s : Type u) × (↑t : Type u)) = #((↑s : Type u) × (↑t : Type u))
⊢ #(↑(s ×ˢ t) : Type u) = #(↑s : Type u) * #(↑t : Type u)

Tactic:
rw [mul_def, mk_congr (Equiv.Set.prod ..)]

Premises used: Cardinal.mul_def, Equiv.Set.prod, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
s : Set α
⊢ #(↑(f '' s) : Type u) ≤ #(↑s : Type u)

Tactic:
mk_le_of_surjective imageFactorization_surjective

Premises used: Cardinal.mk_le_of_surjective, Set.imageFactorization_surjective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
rw : #(↑(uncurry f '' s ×ˢ t) : Type u) ≤ #(↑(s ×ˢ t) : Type u)
⊢ #(↑(image2 f s t) : Type u) ≤ #(↑s : Type u) * #(↑t : Type u)

Tactic:
rw [← image_uncurry_prod, ← mk_setProd]

Premises used: Cardinal.mk_setProd, Set.image_uncurry_prod
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #(↑(uncurry f '' s ×ˢ t) : Type u) ≤ #(↑(s ×ˢ t) : Type u)

Tactic:
mk_image_le

Premises used: Cardinal.mk_image_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #(↑(uncurry f '' s ×ˢ t) : Type u) ≤ #(↑(s ×ˢ t) : Type u)

Tactic:
exact mk_image_le

Premises used: Cardinal.mk_image_le
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : Set α
⊢ lift.{u, v} #(↑(f '' s) : Type v) ≤ lift.{v, u} #(↑s : Type u)

Tactic:
lift_mk_le.{0}.mpr ⟨Embedding.ofSurjective _ imageFactorization_surjective⟩

Premises used: Iff.mpr, Cardinal.lift_mk_le, Function.Embedding.ofSurjective, Nonempty.intro, Set.imageFactorization_surjective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
⊢ #(↑(range f) : Type u) ≤ #α

Tactic:
mk_le_of_surjective rangeFactorization_surjective

Premises used: Cardinal.mk_le_of_surjective, Set.rangeFactorization_surjective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
β : Type v
f : α → β
⊢ lift.{u, v} #(↑(range f) : Type v) ≤ lift.{v, u} #α

Tactic:
lift_mk_le.{0}.mpr ⟨Embedding.ofSurjective _ rangeFactorization_surjective⟩

Premises used: Iff.mpr, Cardinal.lift_mk_le, Function.Embedding.ofSurjective, Nonempty.intro, Set.rangeFactorization_surjective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α β : Type u
f : α → β
h : Injective f
⊢ #(↑(range f) : Type u) = #α

Tactic:
mk_congr (Equiv.ofInjective f h).symm

Premises used: Equiv.ofInjective, Equiv.symm, Cardinal.mk_congr