α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this : ord c < ord univ
⊢ ∃ c', c = lift c'
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
⊢ ∃ c', c = lift c'
have := ord_lt_ord.2 h
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this : ord c < Ordinal.univ
⊢ ∃ c', c = lift c'
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this : ord c < ord univ
⊢ ∃ c', c = lift c'
rw [ord_univ] at this
case intro
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this : ord c < Ordinal.univ
o : Ordinal
e : ↑lift.principalSeg.toRelEmbedding o = ord c
⊢ ∃ c', c = lift c'
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this : ord c < Ordinal.univ
⊢ ∃ c', c = lift c'
cases' lift.principalSeg.{u, u + 1}.down.1 (by simpa only [lift.principalSeg_top] ) with o e
case intro
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this✝ : ord c < Ordinal.univ
o : Ordinal
e : ↑lift.principalSeg.toRelEmbedding o = ord c
this : card (ord c) = c
⊢ ∃ c', c = lift c'
case intro
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this : ord c < Ordinal.univ
o : Ordinal
e : ↑lift.principalSeg.toRelEmbedding o = ord c
⊢ ∃ c', c = lift c'
have := card_ord c
case intro
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this✝ : ord c < Ordinal.univ
o : Ordinal
e : ↑lift.principalSeg.toRelEmbedding o = ord c
this : lift (card o) = c
⊢ ∃ c', c = lift c'
case intro
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this✝ : ord c < Ordinal.univ
o : Ordinal
e : ↑lift.principalSeg.toRelEmbedding o = ord c
this : card (ord c) = c
⊢ ∃ c', c = lift c'
rw [← e, lift.principalSeg_coe, ← lift_card] at this
no goals
case intro
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this✝ : ord c < Ordinal.univ
o : Ordinal
e : ↑lift.principalSeg.toRelEmbedding o = ord c
this : lift (card o) = c
⊢ ∃ c', c = lift c'
exact ⟨_, this.symm⟩
no goals
α : Type ?u.234970
β : Type ?u.234973
γ : Type ?u.234976
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
this : ord c < Ordinal.univ
⊢ ?m.235236 < lift.principalSeg.top
simpa only [lift.principalSeg_top]