α : Type ?u.235536
β : Type ?u.235539
γ : Type ?u.235542
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
a : Cardinal
e : lift a = c
h' : a < (#Ordinal)
⊢ ∃ c', c = lift c'
α : Type ?u.235536
β : Type ?u.235539
γ : Type ?u.235542
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
⊢ ∃ c', c = lift c'
let ⟨a, e, h'⟩ := lt_lift_iff.1 h
α : Type ?u.235536
β : Type ?u.235539
γ : Type ?u.235542
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
a : Cardinal
e : lift a = c
h' : a < univ
⊢ ∃ c', c = lift c'
α : Type ?u.235536
β : Type ?u.235539
γ : Type ?u.235542
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
a : Cardinal
e : lift a = c
h' : a < (#Ordinal)
⊢ ∃ c', c = lift c'
rw [← univ_id] at h'
case intro
α : Type ?u.235536
β : Type ?u.235539
γ : Type ?u.235542
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
c' : Cardinal
e : lift (lift c') = c
h' : lift c' < univ
⊢ ∃ c', c = lift c'
α : Type ?u.235536
β : Type ?u.235539
γ : Type ?u.235542
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
a : Cardinal
e : lift a = c
h' : a < univ
⊢ ∃ c', c = lift c'
rcases lt_univ.{u}.1 h' with ⟨c', rfl⟩
no goals
case intro
α : Type ?u.235536
β : Type ?u.235539
γ : Type ?u.235542
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
c' : Cardinal
e : lift (lift c') = c
h' : lift c' < univ
⊢ ∃ c', c = lift c'
exact ⟨c', by simp only [e.symm, lift_lift]⟩
no goals
α : Type ?u.235536
β : Type ?u.235539
γ : Type ?u.235542
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
h : c < univ
c' : Cardinal
e : lift (lift c') = c
h' : lift c' < univ
⊢ c = lift c'
simp only [e.symm, lift_lift]