no goals
α : Type ?u.170585
r : α → α → Prop
⊢ ℵ₀ < univ
simpa using lift_lt_univ' ℵ₀
no goals
α : Type ?u.170585
r : α → α → Prop
⊢ univ ≤ Ordinal.cof (ord univ)
simp
case intro
α : Type ?u.170585
r : α → α → Prop
c : Cardinal
h : lift c < univ
⊢ 2 ^ lift c < univ
α : Type ?u.170585
r : α → α → Prop
c : Cardinal
h : c < univ
⊢ 2 ^ c < univ
rcases lt_univ'.1 h with ⟨c, rfl⟩
case intro
α : Type ?u.170585
r : α → α → Prop
c : Cardinal
h : lift c < univ
⊢ lift (2 ^ c) < univ
case intro
α : Type ?u.170585
r : α → α → Prop
c : Cardinal
h : lift c < univ
⊢ 2 ^ lift c < univ
rw [← lift_two_power.{u, max (u + 1) v}]
no goals
case intro
α : Type ?u.170585
r : α → α → Prop
c : Cardinal
h : lift c < univ
⊢ lift (2 ^ c) < univ
apply lift_lt_univ'