awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
S : Set ℕ
h' : #(↑S : Type) < #ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
this : S.Finite
⊢ ∃ (n : ℕ), lift.{u_1, 0} #(↑S : Type) = (↑n : Cardinal.{u_1})
have lift : ∀ (S : Finset ℕ) (h' : #(↑(↑S : Set ℕ) : Type) < #ℕ) (h : lift.{u_1, 0} #(↑(↑S : Set ℕ) : Type) < ℵ₀),
  ∃ (n : ℕ), lift.{u_1, 0} #(↑(↑S : Set ℕ) : Type) = (↑n : Cardinal.{u_1})
Tactic: lift S to Finset ℕ using this
Cleared hypotheses: S, h', h, this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
S : Set ℕ
h' : #(↑S : Type) < #ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
⊢ ∃ (n : ℕ), lift.{u_1, 0} #(↑S : Type) = (↑n : Cardinal.{u_1})
have suffices : S.Finite
Tactic: suffices S.Finite by
      lift S to Finset ℕ using this
      simp
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
S : Set ℕ
h' : #(↑S : Type) < #ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
⊢ S.Finite
have contrapose! : ∀ (h' : S.Infinite), #ℕ ≤ #(↑S : Type)
Tactic: contrapose! h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
S : Set ℕ
h : lift.{u_1, 0} #(↑S : Type) < ℵ₀
h' : S.Infinite
⊢ #ℕ ≤ #(↑S : Type)
have this : Infinite (↑S : Type)
Tactic: haveI := Infinite.to_subtype h'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ succ c = c + 1
have obtain : ∀ (n : ℕ) (hn : c = (↑n : Cardinal.{u_1})), succ c = c + 1
Tactic: obtain ⟨n, hn⟩ := Cardinal.lt_aleph0.mp h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
n : ℕ
hn : c = (↑n : Cardinal.{u_1})
⊢ succ c = c + 1
have rw : succ (↑n : Cardinal.{u_1}) = HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
Tactic: rw [hn, succ_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
n : ℕ
hn : c = (↑n : Cardinal.{u_1})
rw : succ (↑n : Cardinal.{u_1}) = HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
⊢ succ c = c + 1
have rw₁ : HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1 = HAdd.hAdd (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) 1
Tactic: rw [hn, succ_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
h : ∀ (n : ℕ), (↑n : Cardinal.{u_1}) ≤ c
hn : c < ℵ₀
⊢ False
have rcases : ∀ (n : ℕ) (h : ∀ (n_1 : ℕ), LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑n_1 : Cardinal.{u_1}) (↑n : Cardinal.{u_1}))
  (hn : (↑n : Cardinal.{u_1}) < ℵ₀), False
Tactic: rcases lt_aleph0.1 hn with ⟨n, rfl⟩
Cleared hypotheses: c, h, hn
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
ha : a < ℵ₀
⊢ succ a < ℵ₀
have rcases : ∀ (n : ℕ) (ha : (↑n : Cardinal.{u_1}) < ℵ₀), succ (↑n : Cardinal.{u_1}) < ℵ₀
Tactic: rcases lt_aleph0.1 ha with ⟨n, rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
ha : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ succ (↑n : Cardinal.{u_1}) < ℵ₀
have rw : (↑(n + 1) : Cardinal.{u_1}) < ℵ₀
Tactic: rw [succ_natCast, ← Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
⊢ IsSuccLimit ℵ₀
have rw : ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀
Tactic: rw [Cardinal.isSuccLimit_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
n : ℕ
h : IsSuccLimit.{u + 1} (α := Cardinal.{u}) (↑n.succ : Cardinal.{u})
⊢ False
have h₁ : IsSuccLimit.{u + 1} (α := Cardinal.{u}) (succ (↑n : Cardinal.{u}))
Tactic: rw [Nat.cast_succ, ← succ_natCast] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ¬IsSuccLimit c
have obtain : ∀ (n : ℕ) (h : (↑n : Cardinal.{u_1}) < ℵ₀), ¬IsSuccLimit.{u_1 + 1} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1})
Tactic: obtain ⟨n, rfl⟩ := lt_aleph0.1 h
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
h : IsSuccLimit c
⊢ ℵ₀ ≤ c
have contrapose! : ∀ (h : c < ℵ₀), ¬IsSuccLimit c
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
⊢ ℵ₀.IsStrongLimit
have refine : ∀ (x : Cardinal.{u_1}) (hx : x < ℵ₀), HPow.hPow (α := Cardinal.{u_1}) 2 x < ℵ₀
Tactic: refine ⟨aleph0_ne_zero, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
x : Cardinal.{u_1}
hx : x < ℵ₀
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 x < ℵ₀
have obtain : ∀ (n : ℕ) (hx : (↑n : Cardinal.{u_1}) < ℵ₀),
  HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) 2 (↑n : Cardinal.{u_1}) < ℵ₀
Tactic: obtain ⟨n, rfl⟩ := lt_aleph0.1 hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
ι : Type u
inst : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
n : ℕ
h : Eq.{v + 2} (α := Cardinal.{v}) (⨆ (i : ι), f i) (↑n : Cardinal.{v})
⊢ ∃ (i : ι), f i = (↑n : Cardinal.{v})
have rw : ∃ (i : ι), f i = ⨆ (i : ι), f i
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
⊢ #α = (↑n : Cardinal.{u}) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
have rw : #α = lift.{u, 0} #(Fin n) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
Tactic: rw [← lift_mk_fin, ← lift_uzero #α, lift_mk_eq']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
rw : #α = lift.{u, 0} #(Fin n) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
⊢ #α = (↑n : Cardinal.{u}) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
have rw₁ : lift.{0, u} #α = lift.{u, 0} #(Fin n) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
Tactic: rw [← lift_mk_fin, ← lift_uzero #α, lift_mk_eq']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
n : ℕ
rw : #α = lift.{u, 0} #(Fin n) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
rw₁ : lift.{0, u} #α = lift.{u, 0} #(Fin n) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
⊢ #α = (↑n : Cardinal.{u}) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
have rw₂ : Nonempty.{max 1 (u + 1)} (α ≃ Fin n) ↔ Nonempty.{max 1 (u + 1)} (α ≃ Fin n)
Tactic: rw [← lift_mk_fin, ← lift_uzero #α, lift_mk_eq']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
⊢ #α ≤ ℵ₀ ↔ Countable α
have rw : #α ≤ ℵ₀ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
Tactic: rw [countable_iff_nonempty_embedding, aleph0, ← lift_uzero #α, lift_mk_le']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : #α ≤ ℵ₀ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
⊢ #α ≤ ℵ₀ ↔ Countable α
have rw₁ : #α ≤ lift.{u, 0} #ℕ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
Tactic: rw [countable_iff_nonempty_embedding, aleph0, ← lift_uzero #α, lift_mk_le']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : #α ≤ ℵ₀ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
rw₁ : #α ≤ lift.{u, 0} #ℕ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
⊢ #α ≤ ℵ₀ ↔ Countable α
have rw₂ : lift.{0, u} #α ≤ lift.{u, 0} #ℕ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
Tactic: rw [countable_iff_nonempty_embedding, aleph0, ← lift_uzero #α, lift_mk_le']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : #α ≤ ℵ₀ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
rw₁ : #α ≤ lift.{u, 0} #ℕ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
rw₂ : lift.{0, u} #α ≤ lift.{u, 0} #ℕ ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
⊢ #α ≤ ℵ₀ ↔ Countable α
have rw₃ : Nonempty.{max 1 (u + 1)} (α ↪ ℕ) ↔ Nonempty.{max 1 (u + 1)} (α ↪ ℕ)
Tactic: rw [countable_iff_nonempty_embedding, aleph0, ← lift_uzero #α, lift_mk_le']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
⊢ ℵ₀ < #α ↔ Uncountable α
have rw : ¬#α ≤ ℵ₀ ↔ Uncountable α
Tactic: rw [← not_le, ← not_countable_iff, not_iff_not, mk_le_aleph0_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : ¬#α ≤ ℵ₀ ↔ Uncountable α
⊢ ℵ₀ < #α ↔ Uncountable α
have rw₁ : ¬#α ≤ ℵ₀ ↔ ¬Countable α
Tactic: rw [← not_le, ← not_countable_iff, not_iff_not, mk_le_aleph0_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : ¬#α ≤ ℵ₀ ↔ Uncountable α
rw₁ : ¬#α ≤ ℵ₀ ↔ ¬Countable α
⊢ ℵ₀ < #α ↔ Uncountable α
have rw₂ : #α ≤ ℵ₀ ↔ Countable α
Tactic: rw [← not_le, ← not_countable_iff, not_iff_not, mk_le_aleph0_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : ¬#α ≤ ℵ₀ ↔ Uncountable α
rw₁ : ¬#α ≤ ℵ₀ ↔ ¬Countable α
rw₂ : #α ≤ ℵ₀ ↔ Countable α
⊢ ℵ₀ < #α ↔ Uncountable α
have rw₃ : Countable α ↔ Countable α
Tactic: rw [← not_le, ← not_countable_iff, not_iff_not, mk_le_aleph0_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
m n : ℕ
ha : (↑m : Cardinal.{u_1}) < ℵ₀
hb : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) < ℵ₀
have rw : (↑(m + n) : Cardinal.{u_1}) < ℵ₀
Tactic: rw [← Nat.cast_add]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a : Cardinal.{u_1}
n : ℕ
⊢ (n + 2) • a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀
have rw : (n + 1 = 0 ∨ a < ℵ₀) ∧ a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀
Tactic: rw [succ_nsmul, add_lt_aleph0_iff, nsmul_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
m n : ℕ
ha : (↑m : Cardinal.{u_1}) < ℵ₀
hb : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ HMul.hMul (α := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) < ℵ₀
have rw : (↑(m * n) : Cardinal.{u_1}) < ℵ₀
Tactic: rw [← Nat.cast_mul]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
⊢ a * b < ℵ₀ ↔ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
have refine_1 : ∀ (h : a * b < ℵ₀), a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
refine_1 : ∀ (h : a * b < ℵ₀), a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
⊢ a * b < ℵ₀ ↔ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
have refine_2 : a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀ → a * b < ℵ₀
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
have pos : ∀ (ha : a = 0), a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
pos : ∀ (ha : a = 0), a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
have neg : ∀ (ha : ¬a = 0), a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
have neg : b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Tactic: right
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
have pos : ∀ (hb : b = 0), b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
pos : ∀ (hb : b = 0), b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
have neg : ∀ (hb : ¬b = 0), b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
have neg : a < ℵ₀ ∧ b < ℵ₀
Tactic: right
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a < ℵ₀ ∧ b < ℵ₀
have ha₁ : 1 ≤ a
Tactic: rw [← Ne, ← Cardinal.one_le_iff_ne_zero] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
ha₁ : 1 ≤ a
⊢ a < ℵ₀ ∧ b < ℵ₀
have hb₁ : 1 ≤ b
Tactic: rw [← Ne, ← Cardinal.one_le_iff_ne_zero] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀ ∧ b < ℵ₀
have neg : a < ℵ₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
neg : a < ℵ₀
⊢ a < ℵ₀ ∧ b < ℵ₀
have neg₁ : b < ℵ₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀
have neg : a * 1 < ℵ₀
Tactic: rw [← mul_one a]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ b < ℵ₀
have neg : 1 * b < ℵ₀
Tactic: rw [← one_mul b]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
h : ¬a * b < ℵ₀ ↔ ¬(a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀) := ⋯
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
have rwa : ∀ (h : ℵ₀ ≤ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
have rwa₁ : ∀ (h : ℵ₀ ≤ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
have rwa₂ : ∀ (h : ℵ₀ ≤ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
have rwa₃ : ∀ (h : ℵ₀ ≤ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
have rwa₄ : ∀ (h : ℵ₀ ≤ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
have rwa₅ : ∀ (h : ℵ₀ ≤ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
a b : Cardinal.{u}
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0
have this : ∀ {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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0
have simp : b ≠ 0 ∧ ℵ₀ ≤ a ∨ a ≠ 0 ∧ ℵ₀ ≤ 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)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
a b : Cardinal.{u_1}
m n : ℕ
ha : (↑m : Cardinal.{u_1}) < ℵ₀
hb : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (↑m : Cardinal.{u_1}) (↑n : Cardinal.{u_1}) < ℵ₀
have rw : (↑(m ^ n) : Cardinal.{u_1}) < ℵ₀
Tactic: rw [power_natCast, ← Nat.cast_pow]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
⊢ Infinite α ↔ ℵ₀ ≤ #α
have rw : Infinite α ↔ ¬#α < ℵ₀
Tactic: rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : Infinite α ↔ ¬#α < ℵ₀
⊢ Infinite α ↔ ℵ₀ ≤ #α
have rw₁ : Infinite α ↔ ¬Finite α
Tactic: rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
rw : Infinite α ↔ ¬#α < ℵ₀
rw₁ : Infinite α ↔ ¬Finite α
⊢ Infinite α ↔ ℵ₀ ≤ #α
have rw₂ : Infinite α ↔ Infinite α
Tactic: rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
h : #α = ℵ₀
⊢ Nonempty.{u + 1} (Denumerable α)
have obtain : ∀ (f : α ≃ ULift.{u, 0} ℕ), Nonempty.{u + 1} (Denumerable α)
Tactic: obtain ⟨f⟩ := Quotient.exact h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.Countable ∧ s.Infinite ↔ Nonempty.{u_1 + 1} (Denumerable (↑s : Type u_1))
have rw : s.Countable ∧ s.Infinite ↔ Countable.{u_1 + 1} (↑s : Type u_1) ∧ Infinite.{u_1 + 1} (↑s : Type u_1)
Tactic: rw [nonempty_denumerable_iff, ← Set.infinite_coe_iff, countable_coe_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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)
⊢ s.Countable ∧ s.Infinite ↔ Nonempty.{u_1 + 1} (Denumerable (↑s : Type u_1))
have 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)
Tactic: rw [nonempty_denumerable_iff, ← Set.infinite_coe_iff, countable_coe_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
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)
⊢ s.Countable ∧ s.Infinite ↔ Nonempty.{u_1 + 1} (Denumerable (↑s : Type u_1))
have rw₂ : s.Countable ∧ Infinite.{u_1 + 1} (↑s : Type u_1) ↔ s.Countable ∧ Infinite.{u_1 + 1} (↑s : Type u_1)
Tactic: rw [nonempty_denumerable_iff, ← Set.infinite_coe_iff, countable_coe_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑n : Cardinal.{u_1})
have rwa : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑1 : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
Tactic: rwa [← Nat.cast_one, Nat.cast_le, Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
rwa : LE.le.{u_1 + 1} (α := Cardinal.{u_1}) (↑1 : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
⊢ LE.le.{u_1 + 1} (α := Cardinal.{u_1}) 1 (↑n : Cardinal.{u_1})
have rwa₁ : 1 ≤ n
Tactic: rwa [← Nat.cast_one, Nat.cast_le, Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ ℵ₀ * (↑n : Cardinal.{u_1}) = ℵ₀
have rw : (↑n : Cardinal.{u_1}) * ℵ₀ = ℵ₀
Tactic: rw [mul_comm, nat_mul_aleph0 hn]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : (↑n : Cardinal.{u_1}) * ℵ₀ = ℵ₀
⊢ ℵ₀ * (↑n : Cardinal.{u_1}) = ℵ₀
have rw₁ : ℵ₀ = ℵ₀
Tactic: rw [mul_comm, nat_mul_aleph0 hn]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
⊢ (↑n : Cardinal.{u_1}) + ℵ₀ = ℵ₀
have rw : ℵ₀ + (↑n : Cardinal.{u_1}) = ℵ₀
Tactic: rw [add_comm, aleph0_add_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
n : ℕ
rw : ℵ₀ + (↑n : Cardinal.{u_1}) = ℵ₀
⊢ (↑n : Cardinal.{u_1}) + ℵ₀ = ℵ₀
have rw₁ : ℵ₀ = ℵ₀
Tactic: rw [add_comm, aleph0_add_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
c : Cardinal.{u_1}
n : ℕ
h : c ≤ (↑n : Cardinal.{u_1})
⊢ ∃ m ≤ n, c = (↑m : Cardinal.{u_1})
have 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})
Tactic: lift c to ℕ using h.trans_lt natCast_lt_aleph0
Cleared hypotheses: c, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
⊢ (sum fun (n : ℕ) ↦ HPow.hPow (α := Cardinal.{u_1}) 0 n) = 1
have rw : (sum fun (n : ℕ) ↦ #PEmpty.{u_1 + 1} ^ n) = 1
Tactic: rw [← mk_eq_zero (α := PEmpty), ← mk_list_eq_sum_pow, mk_eq_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
rw : (sum fun (n : ℕ) ↦ #PEmpty.{u_1 + 1} ^ n) = 1
⊢ (sum fun (n : ℕ) ↦ HPow.hPow (α := Cardinal.{u_1}) 0 n) = 1
have rw₁ : #(List PEmpty.{u_1 + 1}) = 1
Tactic: rw [← mk_eq_zero (α := PEmpty), ← mk_list_eq_sum_pow, mk_eq_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
rw : (sum fun (n : ℕ) ↦ #PEmpty.{u_1 + 1} ^ n) = 1
rw₁ : #(List PEmpty.{u_1 + 1}) = 1
⊢ (sum fun (n : ℕ) ↦ HPow.hPow (α := Cardinal.{u_1}) 0 n) = 1
have rw₂ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) 1 1
Tactic: rw [← mk_eq_zero (α := PEmpty), ← mk_list_eq_sum_pow, mk_eq_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ #(↑s : Type u) = 0 ↔ s = ∅
have rw : IsEmpty.{u + 1} (↑s : Type u) ↔ s = ∅
Tactic: rw [mk_eq_zero_iff, isEmpty_coe_sort]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
rw : IsEmpty.{u + 1} (↑s : Type u) ↔ s = ∅
⊢ #(↑s : Type u) = 0 ↔ s = ∅
have rw₁ : s = ∅ ↔ s = ∅
Tactic: rw [mk_eq_zero_iff, isEmpty_coe_sort]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ #(↑s : Type u) ≠ 0 ↔ s.Nonempty
have rw : Nonempty.{u + 1} (↑s : Type u) ↔ s.Nonempty
Tactic: rw [mk_ne_zero_iff, nonempty_coe_sort]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
rw : Nonempty.{u + 1} (↑s : Type u) ↔ s.Nonempty
⊢ #(↑s : Type u) ≠ 0 ↔ s.Nonempty
have rw₁ : s.Nonempty ↔ s.Nonempty
Tactic: rw [mk_ne_zero_iff, nonempty_coe_sort]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α β : Type u
s : Set α
t : Set β
⊢ #(↑(s ×ˢ t) : Type u) = #(↑s : Type u) * #(↑t : Type u)
have rw : #(↑(s ×ˢ t) : Type u) = #((↑s : Type u) × (↑t : Type u))
Tactic: rw [mul_def, mk_congr (Equiv.Set.prod ..)]