awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
apply : Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof
⊢ lsub.{u, v} f < c

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.Cofinality.Ordinal
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
rwa : Cardinal.lift.{v, u} #ι < (lift.{u, max u v} c).cof
rwa₁ rwa₂ rwa₃ rwa₄ : Cardinal.lift.{v, u} #ι < c.cof
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof

Tactic:
rwa [Cardinal.lift_umax, c.lift_id']

Premises used: Cardinal.lift_umax, Ordinal.lift_id'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{u}
c : Ordinal.{u}
hι : #ι < c.cof
⊢ (∀ (i : ι), f i < c) → lsub f < c

Tactic:
iSup_add_one_lt_of_lt_cof hι

Premises used: Order.succ, Ordinal.iSup_add_one_lt_of_lt_cof, Ordinal.lsub
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
by_contra! : ∀ (hf : Cardinal.lift.{v, u} #ι < (iSup f).cof), False
⊢ (iSup f).cof ≤ Cardinal.lift.{v, u} #ι

Tactic:
by_contra! hf
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
apply : Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} (iSup f)).cof
⊢ False

Tactic:
apply (lift_iSup_lt_of_lt_cof _ H).false

Premises used: Ordinal.lift_iSup_lt_of_lt_cof, LT.lt.false
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
rwa : Cardinal.lift.{v, u} #ι < (lift.{u, max u v} (iSup f)).cof
rwa₁ rwa₂ rwa₃ rwa₄ : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} (iSup f)).cof

Tactic:
rwa [Cardinal.lift_umax, lift_id']

Premises used: Cardinal.lift_umax, Ordinal.lift_id'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u_1
f : ι → Ordinal.{u_1}
H : ∀ (i : ι), f i < iSup f
by_contra! : ∀ (hf : #ι < (iSup f).cof), False
⊢ (iSup f).cof ≤ #ι

Tactic:
by_contra! hf
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u_1
f : ι → Ordinal.{u_1}
H : ∀ (i : ι), f i < iSup f
hf : #ι < (iSup f).cof
⊢ False

Tactic:
(iSup_lt_of_lt_cof hf H).false

Premises used: Ordinal.iSup_lt_of_lt_cof, LT.lt.false
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u_1
f : ι → Ordinal.{u_1}
H : ∀ (i : ι), f i < iSup f
hf : #ι < (iSup f).cof
⊢ False

Tactic:
exact (iSup_lt_of_lt_cof hf H).false

Premises used: Ordinal.iSup_lt_of_lt_cof, LT.lt.false
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
apply : Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof
⊢ iSup f < c

Tactic:
apply lift_iSup_lt_of_lt_cof _ hf

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

Tactic:
rwa [Cardinal.lift_umax, lift_id']

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

Tactic:
apply lift_iSup_lt_of_lt_cof_ord _ hf

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

Tactic:
rwa [Cardinal.lift_umax, c.lift_id']

Premises used: Cardinal.lift_id', Cardinal.lift_umax
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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

Tactic:
lift_iSup_lt_of_lt_cof ?_ (fun l ↦ ?_)

Premises used: Ordinal.nfpFamily, Ordinal.lift_iSup_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
refine_2 : ∀ (l : List ι), List.foldr f a l < c
⊢ nfpFamily f a < c

Tactic:
refine lift_iSup_lt_of_lt_cof ?_ (fun l ↦ ?_)

Premises used: Ordinal.lift_iSup_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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.{v, u} #(List ι) < c.cof
⊢ Cardinal.lift.{max u v, u} #(List ι) < (lift.{u, max u v} c).cof

Tactic:
rw [Cardinal.lift_umax, c.lift_id']

Premises used: Cardinal.lift_umax, Ordinal.lift_id'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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.{v, u} (max ℵ₀ #ι) < c.cof
⊢ Cardinal.lift.{v, u} #(List ι) < c.cof

Tactic:
apply (Cardinal.lift_le.2 (mk_list_le_max _)).trans_lt

Premises used: Iff.mpr, Cardinal.mk_list_le_max, LE.le.trans_lt, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 : max (Cardinal.lift.{v, u} ℵ₀) (Cardinal.lift.{v, u} #ι) < c.cof
⊢ Cardinal.lift.{v, u} (max ℵ₀ #ι) < c.cof

Tactic:
rw [Cardinal.lift_max]

Premises used: Cardinal.lift_max
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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.{v, u} ℵ₀ < c.cof
refine_1₁ : Cardinal.lift.{v, u} #ι < c.cof
⊢ max (Cardinal.lift.{v, u} ℵ₀) (Cardinal.lift.{v, u} #ι) < c.cof

Tactic:
apply max_lt

Premises used: max_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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} ℵ₀ < c.cof

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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} #ι < c.cof

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ List.foldr f a [] < c

Tactic:
ha

Premises used: List.foldr
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ List.foldr f a [] < c

Tactic:
exact ha
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
i : ι
l : List ι
H : List.foldr f a l < c
⊢ List.foldr f a (i :: l) < c

Tactic:
hf _ _ H

Premises used: List.foldr
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
i : ι
l : List ι
H : List.foldr f a l < c
⊢ List.foldr f a (i :: l) < c

Tactic:
exact hf _ _ H
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
refine_2₁ : ∀ (i : ι) (l : List ι) (H : List.foldr f a l < c), List.foldr f a (i :: l) < c
⊢ List.foldr f a l < c

Tactic:
induction l with
    | nil => exact ha
    | cons i l H => exact hf _ _ H
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Ordinal.{u}
hc : ℵ₀ < c.cof
hc' : #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{u}
rwa rwa₁ rwa₂ rwa₃ : #ι < c.cof
⊢ Cardinal.lift.{u, u} #ι < c.cof

Tactic:
rwa [(#ι).lift_id]

Premises used: Cardinal.mk, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
c : Ordinal.{u_1}
hc : ℵ₀ < c.cof
hf : ∀ i < c, f i < c
a : Ordinal.{u_1}
⊢ Cardinal.lift.{u_1, 0} #Unit < c.cof

Tactic:
simpa using Cardinal.one_lt_aleph0.trans hc

Premises used: Cardinal.one_lt_aleph0, LT.lt.trans
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
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
⊢ ∃ (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ι⟩

Premises used: Ordinal.exists_lsub_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hι : #ι = o.cof
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
⊢ ∃ (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ι'⟩

Premises used: Cardinal.exists_ord_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ (type r).blsub (bfamilyOfFamily' r f) = o

Tactic:
rw [← @blsub_eq_lsub' ι r hr] at hf

Premises used: Ordinal.blsub_eq_lsub'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
hf₁ : (type r).blsub (bfamilyOfFamily' r f) = o
⊢ (#ι).ord = type r

Tactic:
rw [← @blsub_eq_lsub' ι r hr] at hf

Premises used: Ordinal.blsub_eq_lsub'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
rw : ∃ (f : (a : Ordinal.{u}) → a < type r → Ordinal.{u}), (type r).blsub f = o
⊢ ∃ (f : (a : Ordinal.{u}) → a < o.cof.ord → Ordinal.{u}), o.cof.ord.blsub f = o

Tactic:
rw [← hι, hι']
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 < type r → Ordinal.{u}), (type r).blsub f = o

Tactic:
⟨_, hf⟩

Premises used: Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 < type r → Ordinal.{u}), (type r).blsub f = o

Tactic:
exact ⟨_, hf⟩
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = b → a ≤ #ι
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
hf : o.blsub f = b
⊢ a ≤ o.card

Tactic:
simpa using H _ hf
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
rcases : ∀ (r : ι → ι → Prop) (hr : IsWellOrder ι r) (hι' : (#ι).ord = type r), a ≤ #ι
⊢ a ≤ #ι

Tactic:
rcases Cardinal.exists_ord_eq ι with ⟨r, hr, hι'⟩

Premises used: Cardinal.exists_ord_eq
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ (type r).blsub (bfamilyOfFamily' r f) = b

Tactic:
rw [← @blsub_eq_lsub' ι r hr] at hf

Premises used: Ordinal.blsub_eq_lsub'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
hf₁ : (type r).blsub (bfamilyOfFamily' r f) = b
⊢ (#ι).ord = type r

Tactic:
rw [← @blsub_eq_lsub' ι r hr] at hf

Premises used: Ordinal.blsub_eq_lsub'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι

Tactic:
simpa using H _ hf
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
rw : (blsub.{u, v} o f).cof ≤ Cardinal.lift.{v, u} #o.ToType
⊢ (blsub.{u, v} o f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
rw [← mk_toType o]

Premises used: Cardinal.mk_toType
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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.ToType

Tactic:
cof_lsub_le_lift _

Premises used: Ordinal.cof_lsub_le_lift, Ordinal.familyOfBFamily, Ordinal.bsup, Ordinal.blsub, Ordinal.familyOfBFamily'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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.ToType

Tactic:
exact cof_lsub_le_lift _

Premises used: Ordinal.cof_lsub_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
rw : (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card
⊢ (o.blsub f).cof ≤ o.card

Tactic:
rw [← o.card.lift_id]

Premises used: Ordinal.card, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card

Tactic:
cof_blsub_le_lift f

Premises used: Ordinal.cof_blsub_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card

Tactic:
exact cof_blsub_le_lift f

Premises used: Ordinal.cof_blsub_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Ordinal.{max u v}
ho : Cardinal.lift.{v, u} o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
h : blsub.{u, v} o f = c
⊢ c.cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
simpa [← iSup_ord, hf, h] using cof_blsub_le_lift.{u, v} f

Premises used: Ordinal.iSup_ord
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
rwa rwa₁ rwa₂ rwa₃ : o.card < c.cof
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
rwa [o.card.lift_id]

Premises used: Ordinal.card, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 = blsub.{u, v} o f

Tactic:
rw [← bsup_eq_blsub_iff_lt_bsup.{u, v}] at H
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
rw : (blsub.{u, v} o f).cof ≤ Cardinal.lift.{v, u} o.card
⊢ (bsup.{u, v} o f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
rw [H]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ (blsub.{u, v} o f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
cof_blsub_le_lift.{u, v} f

Premises used: Ordinal.cof_blsub_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
⊢ (blsub.{u, v} o f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
exact cof_blsub_le_lift.{u, v} f
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
rw : (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ Cardinal.lift.{u, u} o.card
⊢ (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ o.card

Tactic:
rw [← o.card.lift_id]

Premises used: Ordinal.card, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 ≤ Cardinal.lift.{u, u} o.card

Tactic:
cof_bsup_le_lift

Premises used: Ordinal.cof_bsup_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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 ≤ Cardinal.lift.{u, u} o.card

Tactic:
exact cof_bsup_le_lift

Premises used: Ordinal.cof_bsup_le_lift
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Ordinal.{max u v}
ho : Cardinal.lift.{v, u} o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
⊢ bsup.{u, v} o f < c

Tactic:
(bsup_le_blsub f).trans_lt (blsub_lt_ord_lift ho hf)

Premises used: Ordinal.blsub_lt_ord_lift, Ordinal.bsup_le_blsub, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho rwa rwa₁ rwa₂ rwa₃ : o.card < c.cof
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
rwa [o.card.lift_id]

Premises used: Ordinal.card, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
inr₁ : ∀ (hb : IsSuccLimit b), (a + b).cof = b.cof
⊢ (a + b).cof = b.cof

Tactic:
rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨c, rfl⟩ | hb)

Premises used: Ordinal.zero_or_succ_or_isSuccLimit, rfl
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a : Ordinal.{u_1}
hb : Ne.{u_1 + 2} (α := Ordinal.{u_1}) 0 0
⊢ (a + 0).cof = cof 0

Tactic:
contradiction
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
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
inr₃ inr₄ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) 1 1
⊢ (a + succ c).cof = (succ c).cof

Tactic:
rw [succ_eq_add_one, ← add_assoc, cof_add_one, cof_add_one]

Premises used: Ordinal.cof_add_one, Order.succ_eq_add_one, add_assoc
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Ordinal.{u_1}
hb_1 : b ≠ 0
hb : IsSuccLimit b
⊢ (a + b).cof = b.cof

Tactic:
cof_map_of_isNormal (isNormal_add_right a) hb

Premises used: Ordinal.cof_map_of_isNormal, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Ordinal.{u_1}
hb_1 : b ≠ 0
hb : IsSuccLimit b
⊢ (a + b).cof = b.cof

Tactic:
exact cof_map_of_isNormal (isNormal_add_right a) hb

Premises used: Ordinal.cof_map_of_isNormal, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
pos : ∀ (hb' : IsMin b), (a * b).cof = b.cof
neg : ∀ (hb' : ¬IsMin b), (a * b).cof = b.cof
⊢ (a * b).cof = b.cof

Tactic:
by_cases hb' : IsMin b

Premises used: IsMin
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
hb' : IsMin b
⊢ (a * b).cof = b.cof

Tactic:
simp [hb'.eq_bot]

Premises used: IsMin.eq_bot
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
hb' : ¬IsMin b
⊢ (a * b).cof = b.cof

Tactic:
cof_map_of_isNormal (isNormal_mul_right ha.pos) ⟨hb', hb⟩

Premises used: Ordinal.isNormal_mul_right, Ne.pos, Ordinal.cof_map_of_isNormal, And.intro
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a b : Ordinal.{u_1}
ha : a ≠ 0
hb : IsSuccPrelimit b
hb' : ¬IsMin b
⊢ (a * b).cof = b.cof

Tactic:
exact cof_map_of_isNormal (isNormal_mul_right ha.pos) ⟨hb', hb⟩

Premises used: Ordinal.isNormal_mul_right, Ne.pos, Ordinal.cof_map_of_isNormal, And.intro
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
pos : ∀ (h : IsMin o), cof ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = o.cof
neg : ∀ (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

Tactic:
by_cases h : IsMin o

Premises used: IsMin
-- 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:
simp [h.eq_bot]

Premises used: IsMin.eq_bot
-- 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:
cof_map_of_isNormal isNormal_preOmega ⟨h, ho⟩

Premises used: Ordinal.cof_map_of_isNormal, Ordinal.isNormal_preOmega, And.intro