awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
inl : ∀ (hα : #α < ℵ₀), ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
have inr : ∀ (hα : ℵ₀ ≤ #α), ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: rcases lt_or_ge #α ℵ₀ with hα | hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite β
hα : ℵ₀ ≤ #α
⊢ ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
have inr : ∀ (a : α) (ha : #α < #(↑(f ⁻¹' {a}) : Type u)), ∃ (a : α), ℵ₀ ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: obtain ⟨a, ha⟩ := infinite_pigeonhole_card_lt f h (aleph0_le_mk β)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Infinite α
⊢ ∃ (a : α), Infinite.{u + 1} (↑(f ⁻¹' {a}) : Type u)
have suffices : Infinite β
Tactic: suffices Infinite β from exists_infinite_fiber f h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
⊢ ∃ (a : α), Uncountable.{u + 1} (↑(f ⁻¹' {a}) : Type u)
have simp_rw : ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: simp_rw [← Cardinal.aleph0_lt_mk_iff, ← aleph_one_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
⊢ ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
have inl : ∀ (hα : #α < ℵ₀), ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: rcases lt_or_ge #α ℵ₀ with hα | hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
inl : ∀ (hα : #α < ℵ₀), ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
have inr : ∀ (hα : ℵ₀ ≤ #α), ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: rcases lt_or_ge #α ℵ₀ with hα | hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : #α < ℵ₀
⊢ #α < (ord ((ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1)).cof
have rw : #α < (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1
Tactic: rw [isRegular_aleph_one.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : ℵ₀ ≤ #α
⊢ ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
have inr : ∀ (a : α) (ha : #α < #(↑(f ⁻¹' {a}) : Type u)),
  ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: obtain ⟨a, ha⟩ := infinite_pigeonhole_card_lt f h (aleph0_le_mk β)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
hα : ℵ₀ ≤ #α
a : α
ha : #α < #(↑(f ⁻¹' {a}) : Type u)
⊢ ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
have inr : ∀ (hα : (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ succ #α) (a : α) (ha : #α < #(↑(f ⁻¹' {a}) : Type u)),
  ∃ (a : α), (ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) 1 ≤ #(↑(f ⁻¹' {a}) : Type u)
Tactic: rw [← Order.succ_le_succ_iff, succ_aleph0] at hα
Cleared hypotheses: hα, a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite β
f : α → Finset β
w : Eq.{u_2 + 1} (α := Set β) (⋃ (a : α), (↑(f a) : Set β)) Set.univ
⊢ #β ≤ #(↑(range f) : Type u_2)
have by_contra : ∀ (h : ¬#β ≤ #(↑(range f) : Type u_2)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite β
f : α → Finset β
w : Eq.{u_2 + 1} (α := Set β) (⋃ (a : α), (↑(f a) : Set β)) Set.univ
h : ¬#β ≤ #(↑(range f) : Type u_2)
⊢ False
have h₁ : #(↑(range f) : Type u_2) < #β
Tactic: simp only [not_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite β
f : α → Finset β
w : Eq.{u_2 + 1} (α := Set β) (⋃ (a : α), (↑(f a) : Set β)) Set.univ
h : #(↑(range f) : Type u_2) < #β
u : ∀ (b : β), ∃ (a : α), b ∈ f a := ⋯
u' : β → (↑(range f) : Type u_2) :=
  fun (b : β) ↦ Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f (⋯.choose (p := fun (a : α) ↦ b ∈ f a))) ⋯
a : α
p : β
m : p ∈ u' ⁻¹' {Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f a) ⋯}
⊢ p ∈ (↑(f a) : Set β)
have m₁ : f (sorry.choose (p := fun (a : α) ↦ p ∈ f a)) = f a
Tactic: have m : f (u p).choose = f a := by simpa [u'] using m
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite β
f : α → Finset β
w : Eq.{u_2 + 1} (α := Set β) (⋃ (a : α), (↑(f a) : Set β)) Set.univ
h : #(↑(range f) : Type u_2) < #β
u : ∀ (b : β), ∃ (a : α), b ∈ f a := ⋯
u' : β → (↑(range f) : Type u_2) :=
  fun (b : β) ↦ Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f (⋯.choose (p := fun (a : α) ↦ b ∈ f a))) ⋯
a : α
p : β
m_1 : p ∈ u' ⁻¹' {Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f a) ⋯}
m : f (⋯.choose (p := fun (a : α) ↦ p ∈ f a)) = f a
⊢ p ∈ (↑(f a) : Set β)
have rw : p ∈ (↑(f (sorry.choose (p := fun (a : α) ↦ p ∈ f a))) : Set β)
Tactic: rw [← m]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite β
f : α → Finset β
w : Eq.{u_2 + 1} (α := Set β) (⋃ (a : α), (↑(f a) : Set β)) Set.univ
h : #(↑(range f) : Type u_2) < #β
u : ∀ (b : β), ∃ (a : α), b ∈ f a := ⋯
u' : β → (↑(range f) : Type u_2) :=
  fun (b : β) ↦ Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f (⋯.choose (p := fun (a : α) ↦ b ∈ f a))) ⋯
⊢ False
have v' : ∀ (a : α), u' ⁻¹' {Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f a) sorry} ≤ (↑(f a) : Set β)
Tactic: have v' : ∀ a, u' ⁻¹' {⟨f a, by simp⟩} ≤ f a := by
    rintro a p m
    have m : f (u p).choose = f a := by simpa [u'] using m
    rw [← m]
    apply fun b => (u b).choose_spec
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Pigeonhole (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Infinite β
f : α → Finset β
w : Eq.{u_2 + 1} (α := Set β) (⋃ (a : α), (↑(f a) : Set β)) Set.univ
h : #(↑(range f) : Type u_2) < #β
u : ∀ (b : β), ∃ (a : α), b ∈ f a := ⋯
u' : β → (↑(range f) : Type u_2) :=
  fun (b : β) ↦ Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f (⋯.choose (p := fun (a : α) ↦ b ∈ f a))) ⋯
v' : ∀ (a : α), u' ⁻¹' {Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f a) ⋯} ≤ (↑(f a) : Set β)
⊢ False
have obtain : ∀ (a : α) (p : Infinite.{u_2 + 1} (↑(u' ⁻¹' {Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f a) sorry}) : Type u_2)),
  False
Tactic: obtain ⟨⟨-, ⟨a, rfl⟩⟩, p⟩ := exists_infinite_fiber u' h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
H : IsRegular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)
⊢ Ordinal.cof ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have rw : (ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)).cof = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
Tactic: rw [← ord_aleph, H.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
H : IsRegular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)
rw : (ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)).cof = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ Ordinal.cof ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have rw₁ : Eq (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
  ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
Tactic: rw [← ord_aleph, H.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c.ord
have rw : 0 < c
Tactic: rw [Cardinal.lt_ord, card_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ IsRegular.{u_1} o.cof
have refine : ℵ₀ ≤ o.cof
Tactic: refine ⟨?_, (cof_ord_cof o).ge⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ ℵ₀ ≤ o.cof
have rwa : 1 < o.cof
Tactic: rwa [aleph0_le_cof_iff, one_lt_cof_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (hypothesis)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsRegular.{u_1} (succ c)
have hc₀ : ℵ₀ ≤ succ c
Tactic: have hc₀ := hc.trans (le_succ c)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
⊢ IsRegular.{u_1} (succ c)
have le_cof_ord : succ c ≤ (succ c).ord.cof
Tactic: use hc₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
⊢ succ c ≤ (succ c).ord.cof
have le_cof_ord : ∀ (hc' : (succ c).ord.cof < succ c), False
Tactic: by_contra! hc'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
⊢ False
have le_cof_ord : ∀ (f : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1)) → (↑(Iio (succ c).ord) : Type (u_1 + 1)))
  (hf : IsFundamentalSeq f), False
Tactic: obtain ⟨f, hf⟩ := exists_isFundamentalSeq (o := (succ c).ord) rfl
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1)) → (↑(Iio (succ c).ord) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ False
have le_cof_ord : ⨆ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 < (succ c).ord
Tactic: apply hf.iSup_add_one_eq.not_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1)) → (↑(Iio (succ c).ord) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ ⨆ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 < (succ c).ord
have le_cof_ord : card (⨆ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1) ≤ c
Tactic: rw [← card_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1)) → (↑(Iio (succ c).ord) : Type (u_1 + 1))
hf : IsFundamentalSeq f
⊢ card (⨆ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1) ≤ c
have le_cof_ord : (succ c).ord.cof.ord.card ≤ c
Tactic: refine card_iSup_Iio_le ?_ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1)) → (↑(Iio (succ c).ord) : Type (u_1 + 1))
hf : IsFundamentalSeq f
le_cof_ord : (succ c).ord.cof.ord.card ≤ c
⊢ card (⨆ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1) ≤ c
have le_cof_ord₁ : ∀ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), ((↑(f i) : Ordinal.{u_1}) + 1).card ≤ c
Tactic: refine card_iSup_Iio_le ?_ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1)) → (↑(Iio (succ c).ord) : Type (u_1 + 1))
hf : IsFundamentalSeq f
i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))
⊢ ((↑(f i) : Ordinal.{u_1}) + 1).card ≤ c
have le_cof_ord : (↑(f i) : Ordinal.{u_1}) + 1 < (succ c).ord
Tactic: rw [card_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
⊢ IsRegular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)
have rw : IsRegular.{u_1} (succ ℵ₀)
Tactic: rw [← succ_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ IsRegular.{u_1} ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1))
have rw : IsRegular.{u_1} (succ ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))
Tactic: rw [← succ_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ Ordinal.cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (o + 1)) =
    (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1)
have rw : (ord ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1))).cof =
  (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1)
Tactic: rw [← ord_preAleph, (isRegular_preAleph_add_one h).cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
h : ω ≤ o
rw :
  (ord ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1))).cof =
    (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1)
⊢ Ordinal.cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (o + 1)) =
    (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1)
have rw₁ : Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})
  ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})
Tactic: rw [← ord_preAleph, (isRegular_preAleph_add_one h).cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsRegular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1))
have rw : IsRegular.{u_1} (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))
Tactic: rw [← succ_aleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (hypothesis)
Goal:
κ : Cardinal.{v}
h : κ.IsRegular
⊢ (Cardinal.lift.{u, v} κ).IsRegular
have h₁ : ℵ₀ ≤ κ
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (hypothesis)
Goal:
κ : Cardinal.{v}
h : κ.IsRegular
h₁ : ℵ₀ ≤ κ
⊢ (Cardinal.lift.{u, v} κ).IsRegular
have h₂ : κ ≤ κ.ord.cof
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ (Cardinal.lift.{u, v} κ).IsRegular
have aleph0_le : ℵ₀ ≤ Cardinal.lift.{u, v} κ
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
aleph0_le : ℵ₀ ≤ Cardinal.lift.{u, v} κ
⊢ (Cardinal.lift.{u, v} κ).IsRegular
have le_cof_ord : Cardinal.lift.{u, v} κ ≤ (Cardinal.lift.{u, v} κ).ord.cof
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ Cardinal.lift.{u, v} κ ≤ (Cardinal.lift.{u, v} κ).ord.cof
have le_cof_ord : Cardinal.lift.{u, v} κ ≤ (Ordinal.lift.{u, v} κ.ord).cof
Tactic: rwa [← Cardinal.lift_ord, ← Ordinal.lift_cof, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
le_cof_ord : Cardinal.lift.{u, v} κ ≤ (Ordinal.lift.{u, v} κ.ord).cof
⊢ Cardinal.lift.{u, v} κ ≤ (Cardinal.lift.{u, v} κ).ord.cof
have le_cof_ord₁ : Cardinal.lift.{u, v} κ ≤ Cardinal.lift.{u, v} κ.ord.cof
Tactic: rwa [← Cardinal.lift_ord, ← Ordinal.lift_cof, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ lsub.{u, v} f < c.ord
have apply : lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
Tactic: apply lift_iSup_add_one_lt_of_lt_cof _ hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
have rwa : lift.{v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
Tactic: rwa [lift_umax, c.ord.lift_id', hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
rwa : lift.{v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
⊢ lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
have rwa₁ : lift.{v, u} #ι < c.ord.cof
Tactic: rwa [lift_umax, c.ord.lift_id', hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ iSup f < c.ord
have apply : lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
Tactic: apply Ordinal.lift_iSup_lt_of_lt_cof _ hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
⊢ lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
have rwa : lift.{v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
Tactic: rwa [lift_umax, Ordinal.lift_id', hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c.ord
rwa : lift.{v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
⊢ lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
have rwa₁ : lift.{v, u} #ι < c.ord.cof
Tactic: rwa [lift_umax, Ordinal.lift_id', hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ iSup f < c
have apply : lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof
Tactic: apply lift_iSup_lt_of_lt_cof_ord _ hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof
have rwa : lift.{v, u} #ι < (lift.{u, max u v} c).ord.cof
Tactic: rwa [lift_umax, c.lift_id', hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
rwa : lift.{v, u} #ι < (lift.{u, max u v} c).ord.cof
⊢ lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof
have rwa₁ : lift.{v, u} #ι < c.ord.cof
Tactic: rwa [lift_umax, c.lift_id', hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{max u v}
ι : Type u
f : ι → Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ sum f < c
have apply : lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof
Tactic: apply (sum_le_lift_mk_mul_iSup _).trans_lt <|
    mul_lt_of_lt hc.1 hι (lift_iSup_lt_of_lt_cof_ord _ hf)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{max u v}
ι : Type u
f : ι → Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof
have rwa : lift.{v, u} #ι < (lift.{u, max u v} c).ord.cof
Tactic: rwa [lift_umax, c.lift_id', hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{max u v}
ι : Type u
f : ι → Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
rwa : lift.{v, u} #ι < (lift.{u, max u v} c).ord.cof
⊢ lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof
have rwa₁ : lift.{v, u} #ι < c.ord.cof
Tactic: rwa [lift_umax, c.lift_id', hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
⊢ #(↑(⋃ (i : ι), t i) : Type u) < c ↔ ∀ (i : ι), #(↑(t i) : Type u) < c
have refine : ∀ (h : ∀ (i : ι), #(↑(t i) : Type u) < c), #(↑(⋃ (i : ι), t i) : Type u) < c
Tactic: refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #(↑(t i) : Type u) < c
⊢ #(↑(⋃ (i : ι), t i) : Type u) < c
have apply : #(↑(range fun (i : ι) ↦ t i) : Type u) * ⨆ (s : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑s : Set α) : Type u) < c
Tactic: apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #(↑(t i) : Type u) < c
⊢ #(↑(range fun (i : ι) ↦ t i) : Type u) * ⨆ (s : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑s : Set α) : Type u) < c
have apply : ⨆ (s : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑s : Set α) : Type u) < c
Tactic: apply Cardinal.mul_lt_of_lt hc.aleph0_le (mk_range_le.trans_lt hι)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #(↑(t i) : Type u) < c
⊢ ⨆ (s : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑s : Set α) : Type u) < c
have apply : ∀ (i : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑i : Set α) : Type u) < c
Tactic: apply Cardinal.iSup_lt_of_lt_cof_ord (mk_range_le.trans_lt _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #(↑(t i) : Type u) < c
apply : ∀ (i : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑i : Set α) : Type u) < c
⊢ ⨆ (s : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑s : Set α) : Type u) < c
have apply₁ : #ι < c.ord.cof
Tactic: apply Cardinal.iSup_lt_of_lt_cof_ord (mk_range_le.trans_lt _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #(↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) : Type u) < c
a : α
ha : a ∈ s
⊢ #(↑(t a ha) : Type u) < c
have rw : ∀ (h : #(↑(⋃ (x : (↑s : Type u)), t (↑x : α) sorry) : Type u) < c) (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
Tactic: rw [biUnion_eq_iUnion] at h
Cleared hypotheses: h, a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (hypothesis)
Goal:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #(↑(⋃ (x : (↑s : Type u)), t (↑x : α) ⋯) : Type u) < c
a : α
ha : a ∈ s
⊢ #(↑(t a ha) : Type u) < c
have this : ∀ (i : (↑s : Type u)), #(↑(t (↑i : α) sorry) : Type u) < c
Tactic: have := card_lt_of_card_iUnion_lt h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u}
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
hc : c.IsRegular
hs : #(↑s : Type u) < c
⊢ #(↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) : Type u) < c ↔ ∀ (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
have rw : #(↑(⋃ (x : (↑s : Type u)), t (↑x : α) sorry) : Type u) < c ↔ ∀ (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
Tactic: rw [biUnion_eq_iUnion, card_iUnion_lt_iff_forall_of_isRegular hc hs, SetCoe.forall']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u}
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
hc : c.IsRegular
hs : #(↑s : Type u) < c
rw : #(↑(⋃ (x : (↑s : Type u)), t (↑x : α) ⋯) : Type u) < c ↔ ∀ (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
⊢ #(↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) : Type u) < c ↔ ∀ (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
have rw₁ : (∀ (i : (↑s : Type u)), #(↑(t (↑i : α) sorry) : Type u) < c) ↔ ∀ (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
Tactic: rw [biUnion_eq_iUnion, card_iUnion_lt_iff_forall_of_isRegular hc hs, SetCoe.forall']