α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : o < Ordinal.univ
⊢ card o < univ
α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ord univ = Ordinal.univ
refine' le_antisymm (ord_card_le _) <| le_of_forall_lt fun o h => lt_ord.2 ?_
α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : o < Ordinal.univ
this : ∃ a, ↑lift.principalSeg.toRelEmbedding a = o
⊢ card o < univ
α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : o < Ordinal.univ
⊢ card o < univ
have := lift.principalSeg.{u, v}.down.1 (by simpa only [lift.principalSeg_coe] using h)
case intro
α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o✝ : Ordinal
h : o✝ < Ordinal.univ
o : Ordinal
h' : ↑lift.principalSeg.toRelEmbedding o = o✝
⊢ card o✝ < univ
α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : o < Ordinal.univ
this : ∃ a, ↑lift.principalSeg.toRelEmbedding a = o
⊢ card o < univ
rcases this with ⟨o, h'⟩
case intro
α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o✝ : Ordinal
h : o✝ < Ordinal.univ
o : Ordinal
h' : ↑lift.principalSeg.toRelEmbedding o = o✝
⊢ lift (card o) < univ
case intro
α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o✝ : Ordinal
h : o✝ < Ordinal.univ
o : Ordinal
h' : ↑lift.principalSeg.toRelEmbedding o = o✝
⊢ card o✝ < univ
rw [←h', lift.principalSeg_coe, ← lift_card]
no goals
case intro
α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o✝ : Ordinal
h : o✝ < Ordinal.univ
o : Ordinal
h' : ↑lift.principalSeg.toRelEmbedding o = o✝
⊢ lift (card o) < univ
apply lift_lt_univ'
no goals
α : Type ?u.234443
β : Type ?u.234446
γ : Type ?u.234449
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
h : o < Ordinal.univ
⊢ ?m.234736 < lift.principalSeg.top
simpa only [lift.principalSeg_coe] using h