case intro.intro.intro
α : Type ?u.37034
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
hι : (#ι) = cof o
⊢ ∃ f, blsub (ord (cof o)) f = o
α : Type ?u.37034
r : α → α → Prop
o : Ordinal
⊢ ∃ f, blsub (ord (cof o)) f = o
rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩
case intro.intro.intro.intro.intro
α : Type ?u.37034
r✝ : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
hι : (#ι) = cof o
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : ord (#ι) = type r
⊢ ∃ f, blsub (ord (cof o)) f = o
case intro.intro.intro
α : Type ?u.37034
r : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
hι : (#ι) = cof o
⊢ ∃ f, blsub (ord (cof o)) f = o
rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩
case intro.intro.intro.intro.intro
α : Type ?u.37034
r✝ : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hι : (#ι) = cof o
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : blsub (type r) (bfamilyOfFamily' r f) = o
hι' : ord (#ι) = type r
⊢ ∃ f, blsub (ord (cof o)) f = o
case intro.intro.intro.intro.intro
α : Type ?u.37034
r✝ : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hf : lsub f = o
hι : (#ι) = cof o
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : ord (#ι) = type r
⊢ ∃ f, blsub (ord (cof o)) f = o
rw [← @blsub_eq_lsub' ι r hr] at hf
case intro.intro.intro.intro.intro
α : Type ?u.37034
r✝ : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hι : (#ι) = cof o
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : blsub (type r) (bfamilyOfFamily' r f) = o
hι' : ord (#ι) = type r
⊢ ∃ f, blsub (type r) f = o
case intro.intro.intro.intro.intro
α : Type ?u.37034
r✝ : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hι : (#ι) = cof o
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : blsub (type r) (bfamilyOfFamily' r f) = o
hι' : ord (#ι) = type r
⊢ ∃ f, blsub (ord (cof o)) f = o
rw [← hι, hι']
no goals
case intro.intro.intro.intro.intro
α : Type ?u.37034
r✝ : α → α → Prop
o : Ordinal
ι : Type u
f : ι → Ordinal
hι : (#ι) = cof o
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : blsub (type r) (bfamilyOfFamily' r f) = o
hι' : ord (#ι) = type r
⊢ ∃ f, blsub (type r) f = o
exact ⟨_, hf⟩