α : Type ?u.28294
r : α → α → Prop
o : Ordinal
a : Cardinal
⊢ a ≤ sInf {a | ∃ ι f, lsub f = o ∧ (#ι) = a} ↔ ∀ {ι : Type u} (f : ι → Ordinal), lsub f = o → a ≤ (#ι)
α : Type ?u.28294
r : α → α → Prop
o : Ordinal
a : Cardinal
⊢ a ≤ cof o ↔ ∀ {ι : Type u} (f : ι → Ordinal), lsub f = o → a ≤ (#ι)
rw [cof_eq_sInf_lsub]
no goals
α : Type ?u.28294
r : α → α → Prop
o : Ordinal
a : Cardinal
⊢ a ≤ sInf {a | ∃ ι f, lsub f = o ∧ (#ι) = a} ↔ ∀ {ι : Type u} (f : ι → Ordinal), lsub f = o → a ≤ (#ι)
exact
  (le_csInf_iff'' (cof_lsub_def_nonempty o)).trans
    ⟨fun H ι f hf => H _ ⟨ι, f, hf, rfl⟩, fun H b ⟨ι, f, hf, hb⟩ => by
      rw [← hb]
      exact H _ hf⟩
α : Type ?u.28294
r : α → α → Prop
o : Ordinal
a : Cardinal
H : ∀ {ι : Type u} (f : ι → Ordinal), lsub f = o → a ≤ (#ι)
b : Cardinal
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
ι : Type u
f : ι → Ordinal
hf : lsub f = o
hb : (#ι) = b
⊢ a ≤ (#ι)
α : Type ?u.28294
r : α → α → Prop
o : Ordinal
a : Cardinal
H : ∀ {ι : Type u} (f : ι → Ordinal), lsub f = o → a ≤ (#ι)
b : Cardinal
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
ι : Type u
f : ι → Ordinal
hf : lsub f = o
hb : (#ι) = b
⊢ a ≤ b
rw [← hb]
no goals
α : Type ?u.28294
r : α → α → Prop
o : Ordinal
a : Cardinal
H : ∀ {ι : Type u} (f : ι → Ordinal), lsub f = o → a ≤ (#ι)
b : Cardinal
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ (#ι) = a}
ι : Type u
f : ι → Ordinal
hf : lsub f = o
hb : (#ι) = b
⊢ a ≤ (#ι)
exact H _ hf