awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : ¬IsMin o
⊢ cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = o.cof

Tactic:
exact cof_map_of_isNormal isNormal_preOmega ⟨h, ho⟩

Premises used: Ordinal.cof_map_of_isNormal, Ordinal.isNormal_preOmega, And.intro
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ cof ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = o.cof

Tactic:
cof_map_of_isNormal isNormal_omega ho

Premises used: Ordinal.cof_map_of_isNormal, Ordinal.isNormal_omega
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this : LinearOrder α := linearOrderOfSTO r
⊢ WellFoundedLT α

Tactic:
have : WellFoundedLT α := H.toIsWellFounded
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this_1 : LinearOrder α := linearOrderOfSTO r
this : WellFoundedLT α
⊢ NoMaxOrder α

Tactic:
have : NoMaxOrder α := isSuccPrelimit_type_lt_iff.1 h.isSuccPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this_1 : LinearOrder α := linearOrderOfSTO r
this_2 : WellFoundedLT α
this : NoMaxOrder α
obtain :
  ∀ (s : Set α) (hs : IsCofinal s) (hs' : #(↑s : Type u) = Order.cof α),
    ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_cof_eq α

Premises used: Order.exists_cof_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this_1 : LinearOrder α := linearOrderOfSTO r
this_2 : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = Order.cof α
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof

Tactic:
⟨s, ?_, hs'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this_1 : LinearOrder α := linearOrderOfSTO r
this_2 : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = Order.cof α
refine : ∀ (a : α), ∃ b ∈ s, r a b
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof

Tactic:
refine ⟨s, ?_, hs'⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this_1 : LinearOrder α := linearOrderOfSTO r
this_2 : WellFoundedLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : #(↑s : Type u) = Order.cof α
rwa : ∀ (hs : ¬BddAbove s) (hs' : #(↑s : Type u) = Order.cof α) (a : α), ∃ b ∈ s, r a b
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hs : ∀ (x : α), ∃ y ∈ s, x < y) (hs' : #(↑s : Type u) = Order.cof α) (a : α), ∃ b ∈ s, r a b
⊢ ∀ (a : α), ∃ b ∈ s, r a b

Tactic:
rwa [← not_bddAbove_iff_isCofinal, not_bddAbove_iff] at hs

Premises used: not_bddAbove_iff_isCofinal, not_bddAbove_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
let let₁ let₂ : ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
let₃ :
  let this := linearOrderOfSTO r;
  ∀ (this : WellFoundedLT α), ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
let₄ :
  let this := linearOrderOfSTO r;
  ∀ (this_1 : WellFoundedLT α) (this : NoMaxOrder α),
    ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
let₅ :
  let this := linearOrderOfSTO r;
  ∀ (this_1 : WellFoundedLT α) (this_2 : NoMaxOrder α) (s : Set α) (hs : IsCofinal s)
    (hs' : #(↑s : Type u) = Order.cof α), ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
let₆ :
  let this := linearOrderOfSTO r;
  ∀ (this_1 : WellFoundedLT α) (this_2 : NoMaxOrder α) (s : Set α) (hs : IsCofinal s)
    (hs' : #(↑s : Type u) = Order.cof α) (a : α), ∃ b ∈ s, r a b
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof

Tactic:
classical
  let := linearOrderOfSTO r
  have : WellFoundedLT α := H.toIsWellFounded
  have : NoMaxOrder α := isSuccPrelimit_type_lt_iff.1 h.isSuccPrelimit
  obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
  refine ⟨s, ?_, hs'⟩
  rwa [← not_bddAbove_iff_isCofinal, not_bddAbove_iff] at hs

Premises used: not_bddAbove_iff_isCofinal, not_bddAbove_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
apply : univ.{u, v}.card ≤ univ.{u, v}.cof
⊢ univ.{u, v}.cof = Cardinal.univ.{u, v}

Tactic:
apply (cof_le_card _).antisymm

Premises used: LE.le.antisymm, Ordinal.cof_le_card
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
simp_rw : ∀ (s : Set Ordinal.{u}), ¬BddAbove s → #Ordinal.{u} ≤ #(↑s : Type (u + 1))
⊢ univ.{u, v}.card ≤ univ.{u, v}.cof

Tactic:
simp_rw [univ, ← lift_cof, ← lift_card, Cardinal.lift_le, cof_type, card_type, le_cof_iff,
    ← not_bddAbove_iff_isCofinal]

Premises used: Ordinal.cof_type, Ordinal.univ, not_bddAbove_iff_isCofinal, Ordinal.lift_cof, Ordinal.card_type, Ordinal.lift_card, Order.le_cof_iff, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
⊢ ∀ (s : Set Ordinal.{u}), ¬BddAbove s → #Ordinal.{u} ≤ #(↑s : Type (u + 1))

Tactic:
fun s hs ↦ mk_le_of_injective (enumOrdOrderIso s hs).injective

Premises used: Ordinal.enumOrdOrderIso, OrderIso.injective, Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
⊢ ∀ (s : Set Ordinal.{u}), ¬BddAbove s → #Ordinal.{u} ≤ #(↑s : Type (u + 1))

Tactic:
exact fun s hs ↦ mk_le_of_injective (enumOrdOrderIso s hs).injective

Premises used: Ordinal.enumOrdOrderIso, OrderIso.injective, Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
inl : ∀ (ha : #α = 0), #{ s : Set α // Bounded r s } = #α
inr : ∀ (ha : #α ≠ 0), #{ s : Set α // Bounded r s } = #α
⊢ #{ s : Set α // Bounded r s } = #α

Tactic:
rcases eq_or_ne #α 0 with (ha | ha)

Premises used: Cardinal.mk, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
inl : #{ s : Set α // Bounded r s } = 0
⊢ #{ s : Set α // Bounded r s } = #α

Tactic:
rw [ha]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
⊢ IsEmpty α

Tactic:
haveI := mk_eq_zero_iff.1 ha
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
inl : IsEmpty.{u_1 + 1} { s : Set α // Bounded r s }
⊢ #{ s : Set α // Bounded r s } = 0

Tactic:
rw [mk_eq_zero_iff]

Premises used: Cardinal.mk_eq_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
inl : ∀ (a : { s : Set α // Bounded r s }), False
⊢ IsEmpty.{u_1 + 1} { s : Set α // Bounded r s }

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
s : Set α
hs : Bounded r s
⊢ False

Tactic:
(not_unbounded_iff s).2 hs (unbounded_of_isEmpty s)

Premises used: Iff.mpr, Set.unbounded_of_isEmpty, Set.not_unbounded_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
s : Set α
hs : Bounded r s
⊢ False

Tactic:
exact (not_unbounded_iff s).2 hs (unbounded_of_isEmpty s)

Premises used: Iff.mpr, Set.unbounded_of_isEmpty, Set.not_unbounded_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
⊢ IsStrongLimit.{u_1} #α

Tactic:
have h' : IsStrongLimit #α := ⟨ha, @h⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
⊢ ℵ₀ ≤ #α

Tactic:
have ha := h'.aleph0_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
inr : #{ s : Set α // Bounded r s } ≤ #α
inr₁ : #α ≤ #{ s : Set α // Bounded r s }
⊢ #{ s : Set α // Bounded r s } = #α

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
⊢ Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})

Tactic:
have : { s : Set α | Bounded r s } = ⋃ i, 𝒫 { j | r j i } := setOf_exists _
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
inr : #(↑(⋃ (i : α), 𝒫 {j : α | r j i}) : Type u_1) ≤ #α
⊢ #{ s : Set α // Bounded r s } ≤ #α

Tactic:
rw [← coe_setOf, this]

Premises used: Set.coe_setOf
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
⊢ #(↑(⋃ (i : α), 𝒫 {j : α | r j i}) : Type u_1) ≤ #α

Tactic:
mk_iUnion_le_sum_mk.trans ((sum_le_mk_mul_iSup (fun i => #(𝒫 { j | r j i }))).trans
      ((mul_le_max_of_aleph0_le_left ha).trans ?_))

Premises used: Cardinal.sum_le_mk_mul_iSup, setOf, Set.powerset, Cardinal.mk, Cardinal.mk_iUnion_le_sum_mk, Set.Elem, Cardinal.mul_le_max_of_aleph0_le_left, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
inr : max (#α) (⨆ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1)) ≤ #α
⊢ #(↑(⋃ (i : α), 𝒫 {j : α | r j i}) : Type u_1) ≤ #α

Tactic:
refine mk_iUnion_le_sum_mk.trans ((sum_le_mk_mul_iSup (fun i => #(𝒫 { j | r j i }))).trans
      ((mul_le_max_of_aleph0_le_left ha).trans ?_))

Premises used: Cardinal.sum_le_mk_mul_iSup, setOf, Set.powerset, Cardinal.mk, Cardinal.mk_iUnion_le_sum_mk, Set.Elem, Cardinal.mul_le_max_of_aleph0_le_left, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
inr : ⨆ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1) ≤ #α
⊢ max (#α) (⨆ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1)) ≤ #α

Tactic:
rw [max_eq_left]

Premises used: max_eq_left
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
apply : ∀ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1) ≤ #α
⊢ ⨆ (i : α), #(↑(𝒫 {j : α | r j i}) : Type u_1) ≤ #α

Tactic:
apply ciSup_le' _

Premises used: ciSup_le'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
i : α
rw : HPow.hPow (α := Cardinal.{u_1}) 2 #(↑{j : α | r j i} : Type u_1) ≤ #α
⊢ #(↑(𝒫 {j : α | r j i}) : Type u_1) ≤ #α

Tactic:
rw [mk_powerset]

Premises used: Cardinal.mk_powerset
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
i : α
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 #(↑{j : α | r j i} : Type u_1) ≤ #α

Tactic:
(h (card_typein_lt _ hr)).le

Premises used: Set.Mem, setOf, LT.lt.le, Cardinal.card_typein_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
this : Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | Bounded r s} (⋃ (i : α), 𝒫 {j : α | r j i})
i : α
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 #(↑{j : α | r j i} : Type u_1) ≤ #α

Tactic:
exact (h (card_typein_lt _ hr)).le

Premises used: LT.lt.le, Cardinal.card_typein_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
⊢ #α ≤ #{ s : Set α // Bounded r s }

Tactic:
@mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_

Premises used: Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
inr : ∀ (x : α), Bounded r {x}
inr₁ : Injective (β := { s : Set α // Bounded r s }) fun (x : α) ↦ Subtype.mk (p := fun (s : Set α) ↦ Bounded r s) {x} ⋯
⊢ #α ≤ #{ s : Set α // Bounded r s }

Tactic:
refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_

Premises used: Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
x : α
inr : IsSuccLimit (type r)
⊢ Bounded r {x}

Tactic:
apply bounded_singleton

Premises used: Ordinal.bounded_singleton
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
x : α
inr : IsSuccLimit (#α).ord
⊢ IsSuccLimit (type r)

Tactic:
rw [← hr]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
x : α
⊢ IsSuccLimit (#α).ord

Tactic:
apply isSuccLimit_ord ha

Premises used: Cardinal.isSuccLimit_ord
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha_1 : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
ha : ℵ₀ ≤ #α
a b : α
hab :
  Eq.{u_1 + 1} (α := { s : Set α // Bounded r s })
    ((fun (x : α) ↦ Subtype.mk (p := fun (s : Set α) ↦ Bounded r s) {x} ⋯) a)
    ((fun (x : α) ↦ Subtype.mk (p := fun (s : Set α) ↦ Bounded r s) {x} ⋯) b)
⊢ a = b

Tactic:
simpa [singleton_eq_singleton_iff] using hab

Premises used: Set.singleton_eq_singleton_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
inl : ∀ (ha : #α = 0), #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
inr : ∀ (ha : #α ≠ 0), #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α

Tactic:
rcases eq_or_ne #α 0 with (ha | ha)

Premises used: Cardinal.mk, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α = 0
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α

Tactic:
simp [ha]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
⊢ IsStrongLimit.{u_1} #α

Tactic:
have h' : IsStrongLimit #α := ⟨ha, @h⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
inr :
  ∀ (r : α → α → Prop) (wo : IsWellOrder α r) (hr : (#α).ord = type r),
    #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α

Tactic:
rcases exists_ord_eq α with ⟨r, wo, hr⟩

Premises used: Cardinal.exists_ord_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
inr : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #α
inr₁ : #α ≤ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof }
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } = #α

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
rw : #{ s : Set α // Bounded r s }
| #α

Tactic:
rw [← mk_bounded_subset h hr]

Premises used: Cardinal.mk_bounded_subset
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
inr : #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #{ s : Set α // Bounded r s }
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #α

Tactic:
conv_rhs => rw [← mk_bounded_subset h hr]

Premises used: Cardinal.mk_bounded_subset
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
inr : ∀ ⦃x : Set α⦄, #(↑x : Type u_1) < (#α).ord.cof → Bounded r x
⊢ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof } ≤ #{ s : Set α // Bounded r s }

Tactic:
apply mk_subtype_le_of_subset

Premises used: Cardinal.mk_subtype_le_of_subset
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : #(↑s : Type u_1) < (#α).ord.cof
⊢ #(↑s : Type u_1) < (type r).cof

Tactic:
rw [hr] at hs
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : #(↑s : Type u_1) < (type r).cof
inr : ∀ (hs : ¬Bounded r s), (type r).cof ≤ #(↑s : Type u_1)
⊢ Bounded r s

Tactic:
contrapose! hs
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : ¬Bounded r s
⊢ Unbounded r s

Tactic:
rw [not_bounded_iff] at hs

Premises used: Set.not_bounded_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
inr : IsCofinal s
⊢ (type r).cof ≤ #(↑s : Type u_1)

Tactic:
apply cof_le

Premises used: Order.cof_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
inr : ∀ (x : α), ∃ y ∈ s, ¬y < x
⊢ IsCofinal s

Tactic:
simp_rw [IsCofinal, ← not_lt]

Premises used: not_lt, IsCofinal
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ ∀ (x : α), ∃ y ∈ s, ¬y < x

Tactic:
hs

Premises used: Set.Unbounded
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ ∀ (x : α), ∃ y ∈ s, ¬y < x

Tactic:
exact hs
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
⊢ #α ≤ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof }

Tactic:
@mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_

Premises used: Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
inr : ∀ (x : α), #(↑{x} : Type u_1) < (#α).ord.cof
inr₁ :
  Injective (β := { s : Set α // #(↑s : Type u_1) < (#α).ord.cof }) fun (x : α) ↦
    Subtype.mk (p := fun (s : Set α) ↦ #(↑s : Type u_1) < (#α).ord.cof) {x} ⋯
⊢ #α ≤ #{ s : Set α // #(↑s : Type u_1) < (#α).ord.cof }

Tactic:
refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_

Premises used: Cardinal.mk_le_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
x : α
inr : IsSuccLimit (#α).ord
⊢ #(↑{x} : Type u_1) < (#α).ord.cof

Tactic:
rw [mk_singleton, one_lt_cof_iff]

Premises used: Cardinal.mk_singleton, Ordinal.one_lt_cof_iff
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
x : α
⊢ IsSuccLimit (#α).ord

Tactic:
isSuccLimit_ord h'.aleph0_le

Premises used: Cardinal.isSuccLimit_ord, Cardinal.IsStrongLimit.aleph0_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
ha : #α ≠ 0
h' : IsStrongLimit.{u_1} #α
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
x : α
⊢ IsSuccLimit (#α).ord

Tactic:
exact isSuccLimit_ord h'.aleph0_le

Premises used: Cardinal.isSuccLimit_ord, Cardinal.IsStrongLimit.aleph0_le