case intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
c : Cardinal
H : ∀ (S : Set α), Unbounded r S → c ≤ (#↑S)
S : Set α
h : Unbounded r S
⊢ c ≤ (#↑S)
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
c : Cardinal
⊢ (∀ (S : Set α), Unbounded r S → c ≤ (#↑S)) → ∀ (b : Cardinal), b ∈ {c | ∃ S, Unbounded r S ∧ (#↑S) = c} → c ≤ b
rintro H d ⟨S, h, rfl⟩
no goals
case intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
c : Cardinal
H : ∀ (S : Set α), Unbounded r S → c ≤ (#↑S)
S : Set α
h : Unbounded r S
⊢ c ≤ (#↑S)
exact H _ h