α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal
⊢ (∀ (b : Cardinal), b ∈ {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c} → c ≤ b) ↔
    ∀ {S : Set α}, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) → c ≤ (#↑S)
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal
⊢ c ≤ cof r ↔ ∀ {S : Set α}, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) → c ≤ (#↑S)
rw [cof, le_csInf_iff'' (cof_nonempty r)]
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal
⊢ (∀ {S : Set α}, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) → c ≤ (#↑S)) →
    ∀ (b : Cardinal), b ∈ {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c} → c ≤ b
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal
⊢ (∀ (b : Cardinal), b ∈ {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c} → c ≤ b) ↔
    ∀ {S : Set α}, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) → c ≤ (#↑S)
use fun H S h => H _ ⟨S, h, rfl⟩
case intro.intro
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal
H : ∀ {S : Set α}, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) → c ≤ (#↑S)
S : Set α
h : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
⊢ c ≤ (#↑S)
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal
⊢ (∀ {S : Set α}, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) → c ≤ (#↑S)) →
    ∀ (b : Cardinal), b ∈ {c | ∃ S, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) ∧ (#↑S) = c} → c ≤ b
rintro H d ⟨S, h, rfl⟩
no goals
case intro.intro
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsRefl α r
c : Cardinal
H : ∀ {S : Set α}, (∀ (a : α), ∃ b, b ∈ S ∧ r a b) → c ≤ (#↑S)
S : Set α
h : ∀ (a : α), ∃ b, b ∈ S ∧ r a b
⊢ c ≤ (#↑S)
exact H h