no goals
α : Type ?u.37432
r : α → α → Prop
b : Ordinal
a : Cardinal
H : ∀ {ι : Type u} (f : ι → Ordinal), lsub f = b → a ≤ (#ι)
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
hf : blsub o f = b
⊢ a ≤ card o
simpa using H _ hf
case intro.intro
α : Type ?u.37432
r✝ : α → α → Prop
b : Ordinal
a : Cardinal
H : ∀ {o : Ordinal} (f : (a : Ordinal) → a < o → Ordinal), blsub o f = b → a ≤ card o
ι : Type u
f : ι → Ordinal
hf : lsub f = b
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : ord (#ι) = type r
⊢ a ≤ (#ι)
α : Type ?u.37432
r : α → α → Prop
b : Ordinal
a : Cardinal
H : ∀ {o : Ordinal} (f : (a : Ordinal) → a < o → Ordinal), blsub o f = b → a ≤ card o
ι : Type u
f : ι → Ordinal
hf : lsub f = b
⊢ a ≤ (#ι)
rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩
case intro.intro
α : Type ?u.37432
r✝ : α → α → Prop
b : Ordinal
a : Cardinal
H : ∀ {o : Ordinal} (f : (a : Ordinal) → a < o → Ordinal), blsub o f = b → a ≤ card o
ι : Type u
f : ι → Ordinal
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : blsub (type r) (bfamilyOfFamily' r f) = b
hι' : ord (#ι) = type r
⊢ a ≤ (#ι)
case intro.intro
α : Type ?u.37432
r✝ : α → α → Prop
b : Ordinal
a : Cardinal
H : ∀ {o : Ordinal} (f : (a : Ordinal) → a < o → Ordinal), blsub o f = b → a ≤ card o
ι : Type u
f : ι → Ordinal
hf : lsub f = b
r : ι → ι → Prop
hr : IsWellOrder ι r
hι' : ord (#ι) = type r
⊢ a ≤ (#ι)
rw [← @blsub_eq_lsub' ι r hr] at hf
no goals
case intro.intro
α : Type ?u.37432
r✝ : α → α → Prop
b : Ordinal
a : Cardinal
H : ∀ {o : Ordinal} (f : (a : Ordinal) → a < o → Ordinal), blsub o f = b → a ≤ card o
ι : Type u
f : ι → Ordinal
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : blsub (type r) (bfamilyOfFamily' r f) = b
hι' : ord (#ι) = type r
⊢ a ≤ (#ι)
simpa using H _ hf