awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
h :
  Membership.mem (γ := Set Cardinal.{u}) {a : Cardinal.{u} | ∃ (ι : Type u) (f : ι → Ordinal.{u}), lsub f = o ∧ #ι = a}
    b
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ b
have rw : a ≤ #ι
Tactic: rw [← hb]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ lsub.{u, v} f < c
have apply : Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof
Tactic: apply lift_iSup_add_one_lt_of_lt_cof _ hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof
have rwa : Cardinal.lift.{v, u} #ι < (lift.{u, max u v} c).cof
Tactic: rwa [Cardinal.lift_umax, c.lift_id']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
⊢ (iSup f).cof ≤ Cardinal.lift.{v, u} #ι
have by_contra! : ∀ (hf : Cardinal.lift.{v, u} #ι < (iSup f).cof), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ False
have apply : Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} (iSup f)).cof
Tactic: apply (lift_iSup_lt_of_lt_cof _ H).false
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} (iSup f)).cof
have rwa : Cardinal.lift.{v, u} #ι < (lift.{u, max u v} (iSup f)).cof
Tactic: rwa [Cardinal.lift_umax, lift_id']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u_1
f : ι → Ordinal.{u_1}
H : ∀ (i : ι), f i < iSup f
⊢ (iSup f).cof ≤ #ι
have by_contra! : ∀ (hf : #ι < (iSup f).cof), False
Tactic: by_contra! hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ iSup f < c
have apply : Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof
Tactic: apply lift_iSup_lt_of_lt_cof _ hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof
have rwa : Cardinal.lift.{v, u} #ι < (lift.{u, max u v} c).cof
Tactic: rwa [Cardinal.lift_umax, lift_id']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ iSup f < c
have apply : Cardinal.lift.{max u v, u} #ι < (Cardinal.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.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.ord.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{max u v, u} #ι < (Cardinal.lift.{u, max u v} c).ord.cof
have rwa : Cardinal.lift.{v, u} #ι < (Cardinal.lift.{u, max u v} c).ord.cof
Tactic: rwa [Cardinal.lift_umax, c.lift_id']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ nfpFamily f a < c
have refine_1 : Cardinal.lift.{max u v, u} #(List ι) < (lift.{u, max u v} c).cof
Tactic: refine lift_iSup_lt_of_lt_cof ?_ (fun l ↦ ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
refine_1 : Cardinal.lift.{max u v, u} #(List ι) < (lift.{u, max u v} c).cof
⊢ nfpFamily f a < c
have refine_2 : ∀ (l : List ι), List.foldr f a l < c
Tactic: refine lift_iSup_lt_of_lt_cof ?_ (fun l ↦ ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{max u v, u} #(List ι) < (lift.{u, max u v} c).cof
have refine_1 : Cardinal.lift.{v, u} #(List ι) < c.cof
Tactic: rw [Cardinal.lift_umax, c.lift_id']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} #(List ι) < c.cof
have refine_1 : Cardinal.lift.{v, u} (max ℵ₀ #ι) < c.cof
Tactic: apply (Cardinal.lift_le.2 (mk_list_le_max _)).trans_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} (max ℵ₀ #ι) < c.cof
have refine_1 : max (Cardinal.lift.{v, u} ℵ₀) (Cardinal.lift.{v, u} #ι) < c.cof
Tactic: rw [Cardinal.lift_max]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ max (Cardinal.lift.{v, u} ℵ₀) (Cardinal.lift.{v, u} #ι) < c.cof
have refine_1 : Cardinal.lift.{v, u} ℵ₀ < c.cof
Tactic: apply max_lt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
l : List ι
⊢ List.foldr f a l < c
have refine_2 : List.foldr f a [] < c
Tactic: induction l with
    | nil => exact ha
    | cons i l H => exact hf _ _ H
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
l : List ι
refine_2 : List.foldr f a [] < c
⊢ List.foldr f a l < c
have refine_2₁ : ∀ (i : ι) (l : List ι) (H : List.foldr f a l < c), List.foldr f a (i :: l) < c
Tactic: induction l with
    | nil => exact ha
    | cons i l H => exact hf _ _ H
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
⊢ ∃ (f : (a : Ordinal.{u}) → a < o.cof.ord → Ordinal.{u}), o.cof.ord.blsub f = o
have rcases : ∀ (ι : Type u) (f : ι → Ordinal.{u}) (hf : lsub f = o) (hι : #ι = o.cof),
  ∃ (f : (a : Ordinal.{u}) → a < o.cof.ord → Ordinal.{u}), o.cof.ord.blsub f = o
Tactic: rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
⊢ ∃ (f : (a : Ordinal.{u}) → a < o.cof.ord → Ordinal.{u}), o.cof.ord.blsub f = o
have rcases : ∀ (r : ι → ι → Prop) (hr : IsWellOrder ι r) (hι' : (#ι).ord = type r),
  ∃ (f : (a : Ordinal.{u}) → a < o.cof.ord → Ordinal.{u}), o.cof.ord.blsub f = o
Tactic: rcases Cardinal.exists_ord_eq ι with ⟨r, hr, hι'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ ∃ (f : (a : Ordinal.{u}) → a < o.cof.ord → Ordinal.{u}), o.cof.ord.blsub f = o
have hf₁ : (type r).blsub (bfamilyOfFamily' r f) = o
Tactic: rw [← @blsub_eq_lsub' ι r hr] at hf
Cleared hypotheses: hf, hι'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hι : #ι = o.cof
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = o
hι' : (#ι).ord = type r
⊢ ∃ (f : (a : Ordinal.{u}) → a < o.cof.ord → Ordinal.{u}), o.cof.ord.blsub f = o
have rw : ∃ (f : (a : Ordinal.{u}) → a < type r → Ordinal.{u}), (type r).blsub f = o
Tactic: rw [← hι, hι']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = b
⊢ a ≤ #ι
have rcases : ∀ (r : ι → ι → Prop) (hr : IsWellOrder ι r) (hι' : (#ι).ord = type r), a ≤ #ι
Tactic: rcases Cardinal.exists_ord_eq ι with ⟨r, hr, hι'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = b
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : (#ι).ord = type r
⊢ a ≤ #ι
have hf₁ : (type r).blsub (bfamilyOfFamily' r f) = b
Tactic: rw [← @blsub_eq_lsub' ι r hr] at hf
Cleared hypotheses: hf, hι'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (blsub.{u, v} o f).cof ≤ Cardinal.lift.{v, u} o.card
have rw : (blsub.{u, v} o f).cof ≤ Cardinal.lift.{v, u} #o.ToType
Tactic: rw [← mk_toType o]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ o.card
have rw : (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card
Tactic: rw [← o.card.lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (h : i < o), f i h < bsup.{u, v} o f
⊢ (bsup.{u, v} o f).cof ≤ Cardinal.lift.{v, u} o.card
have H₁ : bsup.{u, v} o f = blsub.{u, v} o f
Tactic: rw [← bsup_eq_blsub_iff_lt_bsup.{u, v}] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : bsup.{u, v} o f = blsub.{u, v} o f
⊢ (bsup.{u, v} o f).cof ≤ Cardinal.lift.{v, u} o.card
have rw : (blsub.{u, v} o f).cof ≤ Cardinal.lift.{v, u} o.card
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ o.card
have rw : (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ Cardinal.lift.{u, u} o.card
Tactic: rw [← o.card.lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (a + b).cof = b.cof
have inl : ∀ (hb : Ne.{u_1 + 2} (α := Ordinal.{u_1}) 0 0), (a + 0).cof = cof 0
Tactic: rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨c, rfl⟩ | hb)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
inl : ∀ (hb : Ne.{u_1 + 2} (α := Ordinal.{u_1}) 0 0), (a + 0).cof = cof 0
⊢ (a + b).cof = b.cof
have inr : ∀ (c : Ordinal.{u_1}) (hb : succ c ≠ 0), (a + succ c).cof = (succ c).cof
Tactic: rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨c, rfl⟩ | hb)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
inl : ∀ (hb : Ne.{u_1 + 2} (α := Ordinal.{u_1}) 0 0), (a + 0).cof = cof 0
inr : ∀ (c : Ordinal.{u_1}) (hb : succ c ≠ 0), (a + succ c).cof = (succ c).cof
⊢ (a + b).cof = b.cof
have inr₁ : ∀ (hb : IsSuccLimit b), (a + b).cof = b.cof
Tactic: rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨c, rfl⟩ | hb)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + succ c).cof = (succ c).cof
have inr : (a + (c + 1)).cof = (c + 1).cof
Tactic: rw [succ_eq_add_one, ← add_assoc, cof_add_one, cof_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a c : Ordinal.{u_1}
hb : succ c ≠ 0
inr : (a + (c + 1)).cof = (c + 1).cof
⊢ (a + succ c).cof = (succ c).cof
have inr₁ : (a + c + 1).cof = (c + 1).cof
Tactic: rw [succ_eq_add_one, ← add_assoc, cof_add_one, cof_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a c : Ordinal.{u_1}
hb : succ c ≠ 0
inr : (a + (c + 1)).cof = (c + 1).cof
inr₁ : (a + c + 1).cof = (c + 1).cof
⊢ (a + succ c).cof = (succ c).cof
have inr₂ : 1 = (c + 1).cof
Tactic: rw [succ_eq_add_one, ← add_assoc, cof_add_one, cof_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a c : Ordinal.{u_1}
hb : succ c ≠ 0
inr : (a + (c + 1)).cof = (c + 1).cof
inr₁ : (a + c + 1).cof = (c + 1).cof
inr₂ : 1 = (c + 1).cof
⊢ (a + succ c).cof = (succ c).cof
have inr₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) 1 1
Tactic: rw [succ_eq_add_one, ← add_assoc, cof_add_one, cof_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
⊢ (a * b).cof = b.cof
have pos : ∀ (hb' : IsMin b), (a * b).cof = b.cof
Tactic: by_cases hb' : IsMin b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
pos : ∀ (hb' : IsMin b), (a * b).cof = b.cof
⊢ (a * b).cof = b.cof
have neg : ∀ (hb' : ¬IsMin b), (a * b).cof = b.cof
Tactic: by_cases hb' : IsMin b
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = o.cof
have pos : ∀ (h : IsMin o), cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = o.cof
Tactic: by_cases h : IsMin o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
pos : ∀ (h : IsMin o), cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = o.cof
⊢ cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = o.cof
have neg : ∀ (h : ¬IsMin o), cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = o.cof
Tactic: by_cases h : IsMin o
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this : LinearOrder α := linearOrderOfSTO r
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
have this₁ : WellFoundedLT α
Tactic: have : WellFoundedLT α := H.toIsWellFounded
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (hypothesis)
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this_1 : LinearOrder α := linearOrderOfSTO r
this : WellFoundedLT α
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
have this₁ : NoMaxOrder α
Tactic: have : NoMaxOrder α := isSuccPrelimit_type_lt_iff.1 h.isSuccPrelimit
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u
r : α → α → Prop
H : IsWellOrder α r
h : IsSuccLimit (type r)
this_1 : LinearOrder α := linearOrderOfSTO r
this_2 : WellFoundedLT α
this : NoMaxOrder α
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
have 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
Tactic: obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
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
have refine : ∀ (a : α), ∃ b ∈ s, r a b
Tactic: refine ⟨s, ?_, hs'⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
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 α
⊢ ∀ (a : α), ∃ b ∈ s, r a b
have rwa : ∀ (hs : ¬BddAbove s) (hs' : #(↑s : Type u) = Order.cof α) (a : α), ∃ b ∈ s, r a b
Tactic: rwa [← not_bddAbove_iff_isCofinal, not_bddAbove_iff] at hs
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
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
⊢ ∀ (a : α), ∃ b ∈ s, r a b
have rwa₁ : ∀ (hs : ∀ (x : α), ∃ y ∈ s, x < y) (hs' : #(↑s : Type u) = Order.cof α) (a : α), ∃ b ∈ s, r a b
Tactic: rwa [← not_bddAbove_iff_isCofinal, not_bddAbove_iff] at hs
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
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
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
have let₃ : let this := linearOrderOfSTO r;
∀ (this : WellFoundedLT α), ∃ (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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
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
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
have let₄ : let this := linearOrderOfSTO r;
∀ (this_1 : WellFoundedLT α) (this : NoMaxOrder α),
  ∃ (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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
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
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
have 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
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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
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
⊢ ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) ∧ #(↑S : Type u) = (type r).cof
have 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
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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
⊢ univ.{u, v}.cof = Cardinal.univ.{u, v}
have apply : univ.{u, v}.card ≤ univ.{u, v}.cof
Tactic: apply (cof_le_card _).antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
⊢ univ.{u, v}.card ≤ univ.{u, v}.cof
have simp_rw : ∀ (s : Set Ordinal.{u}), ¬BddAbove s → #Ordinal.{u} ≤ #(↑s : Type (u + 1))
Tactic: simp_rw [univ, ← lift_cof, ← lift_card, Cardinal.lift_le, cof_type, card_type, le_cof_iff,
    ← not_bddAbove_iff_isCofinal]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
⊢ #{ s : Set α // Bounded r s } = #α
have inl : ∀ (ha : #α = 0), #{ s : Set α // Bounded r s } = #α
Tactic: rcases eq_or_ne #α 0 with (ha | ha)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
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 } = #α
⊢ #{ s : Set α // Bounded r s } = #α
have inr : ∀ (ha : #α ≠ 0), #{ s : Set α // Bounded r s } = #α
Tactic: rcases eq_or_ne #α 0 with (ha | ha)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Ordinal (goal)
Goal:
α : Type u_1
h : IsStrongPrelimit.{u_1} #α
r : α → α → Prop
inst : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
⊢ #{ s : Set α // Bounded r s } = #α
have inl : #{ s : Set α // Bounded r s } = 0
Tactic: rw [ha]