awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
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:
⟨a, hα.trans (succ_le_of_lt ha)⟩

Premises used: Order.succ_le_of_lt, Exists.intro, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
β α : Type u
f : β → α
h : #α < #β
inst : Uncountable β
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:
exact ⟨a, hα.trans (succ_le_of_lt ha)⟩
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
Goal:
α : Type u_1
β : Type u_2
inst : Infinite β
f : α → Finset β
w : Eq.{u_2 + 1} (α := Set β) (⋃ (a : α), (↑(f a) : Set β)) Set.univ
by_contra : ∀ (h : ¬#β ≤ #(↑(range f) : Type u_2)), False
⊢ #β ≤ #(↑(range f) : Type u_2)

Tactic:
by_contra h
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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)
⊢ #(↑(range f) : Type u_2) < #β

Tactic:
simp only [not_le] at h

Premises used: not_le
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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) < #β
b : β
⊢ ∃ (a : α), b ∈ f a

Tactic:
simpa using (w.ge :) (Set.mem_univ b)

Premises used: Eq.ge, Set.mem_univ
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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 := ⋯
b : β
⊢ f (⋯.choose (p := fun (a : α) ↦ b ∈ f a)) ∈ range f

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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 : α
⊢ f a ∈ range f

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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) ⋯}
⊢ f (⋯.choose (p := fun (a : α) ↦ p ∈ f a)) = f a

Tactic:
simpa [u'] using m
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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) ⋯}
⊢ f (⋯.choose (p := fun (a : α) ↦ p ∈ f a)) = f a

Tactic:
have m : f (u p).choose = f a := by simpa [u'] using m
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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
rw : p ∈ (↑(f (⋯.choose (p := fun (a : α) ↦ p ∈ f a))) : Set β)
⊢ p ∈ (↑(f a) : Set β)

Tactic:
rw [← m]
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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 (⋯.choose (p := fun (a : α) ↦ p ∈ f a))) : Set β)

Tactic:
apply fun b => (u b).choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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 : α), u' ⁻¹' {Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f a) ⋯} ≤ (↑(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
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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 β)
obtain :
  ∀ (a : α)
    (p : Infinite.{u_2 + 1} (↑(u' ⁻¹' {Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f a) ⋯}) : Type u_2)), False
⊢ False

Tactic:
obtain ⟨⟨-, ⟨a, rfl⟩⟩, p⟩ := exists_infinite_fiber u' h

Premises used: Cardinal.exists_infinite_fiber, rfl
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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 β)
a : α
p : Infinite.{u_2 + 1} (↑(u' ⁻¹' {Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f a) ⋯}) : Type u_2)
⊢ False

Tactic:
(@Infinite.of_injective _ _ p (inclusion (v' a)) (inclusion_injective _)).false

Premises used: Infinite.of_injective, Infinite.false, Set.inclusion_injective, Set.inclusion
-- Module: Mathlib.SetTheory.Cardinal.Pigeonhole
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 β)
a : α
p : Infinite.{u_2 + 1} (↑(u' ⁻¹' {Subtype.mk (p := fun (x : Finset β) ↦ x ∈ range f) (f a) ⋯}) : Type u_2)
⊢ False

Tactic:
exact (@Infinite.of_injective _ _ p (inclusion (v' a)) (inclusion_injective _)).false

Premises used: Infinite.of_injective, Infinite.false, Set.inclusion_injective, Set.inclusion
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ c.ord.cof = c

Tactic:
(cof_ord_le c).antisymm H.2

Premises used: LE.le.antisymm, Ordinal.cof_ord_le, Cardinal.IsRegular.le_cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
rw₁ 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})
⊢ Ordinal.cof ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
rw [← ord_aleph, H.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord, Cardinal.ord_aleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c

Tactic:
aleph0_pos.trans_le H.1

Premises used: Cardinal.IsRegular.aleph0_le, LT.lt.trans_le, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
H : c.IsRegular
n : ℕ
⊢ (↑n : Cardinal.{u_1}) < c

Tactic:
lt_of_lt_of_le natCast_lt_aleph0 H.aleph0_le

Premises used: Cardinal.IsRegular.aleph0_le, Cardinal.natCast_lt_aleph0, lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
H : c.IsRegular
rw : 0 < c
⊢ 0 < c.ord

Tactic:
rw [Cardinal.lt_ord, card_zero]

Premises used: Ordinal.card_zero, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c

Tactic:
H.pos

Premises used: Cardinal.IsRegular.pos
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c

Tactic:
exact H.pos

Premises used: Cardinal.IsRegular.pos
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
h : IsSuccLimit o
⊢ IsRegular.{u_1} o.cof

Tactic:
⟨?_, (cof_ord_cof o).ge⟩

Premises used: Cardinal.IsRegular.mk, Eq.ge, Ordinal.cof_ord_cof
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
h : IsSuccLimit o
refine : ℵ₀ ≤ o.cof
⊢ IsRegular.{u_1} o.cof

Tactic:
refine ⟨?_, (cof_ord_cof o).ge⟩
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
h : IsSuccLimit o
rwa : 1 < o.cof
rwa₁ rwa₂ rwa₃ rwa₄ : IsSuccLimit o
⊢ ℵ₀ ≤ o.cof

Tactic:
rwa [aleph0_le_cof_iff, one_lt_cof_iff]

Premises used: Ordinal.aleph0_le_cof_iff, Ordinal.one_lt_cof_iff
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ c ≠ 0

Tactic:
H.pos.ne'

Premises used: LT.lt.ne', Cardinal.IsRegular.pos
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ ℵ₀ ≤ ℵ₀.ord.cof

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ℵ₀ ≤ succ c

Tactic:
have hc₀ := hc.trans (le_succ c)
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
le_cof_ord : succ c ≤ (succ c).ord.cof
⊢ IsRegular.{u_1} (succ c)

Tactic:
use hc₀
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
le_cof_ord : ∀ (hc' : (succ c).ord.cof < succ c), False
⊢ succ c ≤ (succ c).ord.cof

Tactic:
by_contra! hc'
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
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
⊢ False

Tactic:
obtain ⟨f, hf⟩ := exists_isFundamentalSeq (o := (succ c).ord) rfl

Premises used: Ordinal.exists_isFundamentalSeq, rfl
-- Module: Mathlib.SetTheory.Cardinal.Regular
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 : ⨆ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 < (succ c).ord
⊢ False

Tactic:
apply hf.iSup_add_one_eq.not_lt

Premises used: Eq.not_lt, Ordinal.IsFundamentalSeq.iSup_add_one_eq
-- Module: Mathlib.SetTheory.Cardinal.Regular
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 : card (⨆ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1) ≤ c
⊢ ⨆ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1 < (succ c).ord

Tactic:
rw [← card_le_iff]

Premises used: Cardinal.card_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
card_iSup_Iio_le ?_ fun i ↦ ?_

Premises used: Ordinal.card_iSup_Iio_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
le_cof_ord₁ : ∀ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), ((↑(f i) : Ordinal.{u_1}) + 1).card ≤ c
⊢ card (⨆ (i : (↑(Iio (succ c).ord.cof.ord) : Type (u_1 + 1))), (↑(f i) : Ordinal.{u_1}) + 1) ≤ c

Tactic:
refine card_iSup_Iio_le ?_ fun i ↦ ?_

Premises used: Ordinal.card_iSup_Iio_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
⊢ (succ c).ord.cof.ord.card ≤ c

Tactic:
simpa using hc'
-- Module: Mathlib.SetTheory.Cardinal.Regular
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))
le_cof_ord : (↑(f i) : Ordinal.{u_1}) + 1 < (succ c).ord
⊢ ((↑(f i) : Ordinal.{u_1}) + 1).card ≤ c

Tactic:
rw [card_le_iff]

Premises used: Cardinal.card_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
(isSuccLimit_ord hc₀).add_one_lt (f i).2

Premises used: Cardinal.isSuccLimit_ord, Order.IsSuccLimit.add_one_lt, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
exact (isSuccLimit_ord hc₀).add_one_lt (f i).2

Premises used: Cardinal.isSuccLimit_ord, Order.IsSuccLimit.add_one_lt, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
rw : IsRegular.{u_1} (succ ℵ₀)
⊢ IsRegular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)

Tactic:
rw [← succ_aleph0]

Premises used: Cardinal.succ_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ IsRegular.{u_1} (succ ℵ₀)

Tactic:
isRegular_succ le_rfl

Premises used: le_rfl, Cardinal.isRegular_succ
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ IsRegular.{u_1} (succ ℵ₀)

Tactic:
exact isRegular_succ le_rfl

Premises used: le_rfl, Cardinal.isRegular_succ
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ Ordinal.cof ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1) = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1

Tactic:
simpa using isRegular_aleph_one.cof_omega_eq

Premises used: Cardinal.IsRegular.cof_omega_eq, Cardinal.isRegular_aleph_one
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
α : Type u_1
inst : Countable α
f : α → Ordinal.{u_2}
⊢ lift.{u_2, u_1} #α < (Ordinal.lift.{u_1, u_2} ((ω_ : (a : Ordinal.{u_2}) → Ordinal.{u_2}) 1)).cof

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
h : ω ≤ o
rw : IsRegular.{u_1} (succ ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))
⊢ IsRegular.{u_1} ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1))

Tactic:
rw [← succ_preAleph]

Premises used: Cardinal.succ_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ IsRegular.{u_1} (succ ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))

Tactic:
isRegular_succ (aleph0_le_preAleph.2 h)

Premises used: Iff.mpr, Cardinal.isRegular_succ, Cardinal.aleph0_le_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ IsRegular.{u_1} (succ ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))

Tactic:
exact isRegular_succ (aleph0_le_preAleph.2 h)

Premises used: Iff.mpr, Cardinal.isRegular_succ, Cardinal.aleph0_le_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ IsRegular.{u_1} ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ o))

Tactic:
isRegular_preAleph_add_one h

Premises used: Order.succ, Cardinal.isRegular_preAleph_add_one
-- Module: Mathlib.SetTheory.Cardinal.Regular
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)
rw₁ 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})
⊢ Ordinal.cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (o + 1)) =
    (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1)

Tactic:
rw [← ord_preAleph, (isRegular_preAleph_add_one h).cof_ord]

Premises used: Cardinal.IsRegular.cof_ord, Cardinal.ord_preAleph, Cardinal.isRegular_preAleph_add_one
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
rw : IsRegular.{u_1} (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))
⊢ IsRegular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1))

Tactic:
rw [← succ_aleph]

Premises used: Cardinal.succ_aleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
⊢ IsRegular.{u_1} (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))

Tactic:
isRegular_succ (aleph0_le_aleph o)

Premises used: Cardinal.isRegular_succ, Cardinal.aleph0_le_aleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
⊢ IsRegular.{u_1} (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))

Tactic:
exact isRegular_succ (aleph0_le_aleph o)

Premises used: Cardinal.isRegular_succ, Cardinal.aleph0_le_aleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
⊢ IsRegular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ o))

Tactic:
isRegular_aleph_add_one o

Premises used: Order.succ, Cardinal.isRegular_aleph_add_one
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
⊢ Ordinal.cof ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (o + 1)) = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1)

Tactic:
(isRegular_aleph_add_one o).cof_omega_eq

Premises used: Cardinal.IsRegular.cof_omega_eq, Cardinal.isRegular_aleph_add_one
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
κ : Cardinal.{v}
h : κ.IsRegular
⊢ ℵ₀ ≤ κ

Tactic:
obtain ⟨h₁, h₂⟩ := h
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
κ : Cardinal.{v}
h : κ.IsRegular
h₁ : ℵ₀ ≤ κ
⊢ κ ≤ κ.ord.cof

Tactic:
obtain ⟨h₁, h₂⟩ := h
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
aleph0_le : ℵ₀ ≤ Cardinal.lift.{u, v} κ
le_cof_ord : Cardinal.lift.{u, v} κ ≤ (Cardinal.lift.{u, v} κ).ord.cof
⊢ (Cardinal.lift.{u, v} κ).IsRegular

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ ℵ₀ ≤ Cardinal.lift.{u, v} κ

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
le_cof_ord : Cardinal.lift.{u, v} κ ≤ (Ordinal.lift.{u, v} κ.ord).cof
le_cof_ord₁ : Cardinal.lift.{u, v} κ ≤ Cardinal.lift.{u, v} κ.ord.cof
le_cof_ord₂ le_cof_ord₃ le_cof_ord₄ le_cof_ord₅ : κ ≤ κ.ord.cof
⊢ Cardinal.lift.{u, v} κ ≤ (Cardinal.lift.{u, v} κ).ord.cof

Tactic:
rwa [← Cardinal.lift_ord, ← Ordinal.lift_cof, lift_le]

Premises used: Cardinal.lift_ord, Ordinal.lift_cof, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
κ : Cardinal.{v}
h : (lift.{u, v} κ).IsRegular
h₁ : ℵ₀ ≤ lift.{u, v} κ
h₂ : lift.{u, v} κ ≤ (lift.{u, v} κ).ord.cof
⊢ ℵ₀ ≤ κ

Tactic:
simpa using h₁
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
κ : Cardinal.{v}
h : (lift.{u, v} κ).IsRegular
h₁ : ℵ₀ ≤ lift.{u, v} κ
h₂ : lift.{u, v} κ ≤ (lift.{u, v} κ).ord.cof
⊢ κ ≤ κ.ord.cof

Tactic:
simpa [← lift_le.{u, v}]
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
apply : lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
⊢ lsub.{u, v} f < c.ord

Tactic:
apply lift_iSup_add_one_lt_of_lt_cof _ hf

Premises used: Ordinal.lift_iSup_add_one_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
rwa₁ : lift.{v, u} #ι < c.ord.cof
rwa₂ rwa₃ rwa₄ rwa₅ : lift.{v, u} #ι < c
⊢ lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof

Tactic:
rwa [lift_umax, c.ord.lift_id', hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord, Cardinal.ord, Cardinal.lift_umax, Ordinal.lift_id'
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
ι : Type (max u_1 u_2)
f : ι → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι rwa rwa₁ rwa₂ rwa₃ : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
apply : lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof
⊢ iSup f < c.ord

Tactic:
apply Ordinal.lift_iSup_lt_of_lt_cof _ hf

Premises used: Ordinal.lift_iSup_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
rwa₁ : lift.{v, u} #ι < c.ord.cof
rwa₂ rwa₃ rwa₄ rwa₅ : lift.{v, u} #ι < c
⊢ lift.{max u v, u} #ι < (Ordinal.lift.{u, max u v} c.ord).cof

Tactic:
rwa [lift_umax, Ordinal.lift_id', hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord, Cardinal.lift_umax, Ordinal.lift_id'
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
ι : Type u_1
f : ι → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι rwa rwa₁ rwa₂ rwa₃ : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
ho rwa rwa₁ rwa₂ rwa₃ : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
ho rwa rwa₁ rwa₂ rwa₃ : o.card < c
⊢ o.card < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord