α : Type ?u.234294
β : Type ?u.234297
γ : Type ?u.234300
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
this : lift (lift c) < lift univ
⊢ lift c < univ
α : Type ?u.234294
β : Type ?u.234297
γ : Type ?u.234300
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
⊢ lift c < univ
have := lift_lt.{_, max (u+1) v}.2 (lift_lt_univ c)
α : Type ?u.234294
β : Type ?u.234297
γ : Type ?u.234300
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
this : lift c < univ
⊢ lift c < univ
α : Type ?u.234294
β : Type ?u.234297
γ : Type ?u.234300
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
this : lift (lift c) < lift univ
⊢ lift c < univ
rw [lift_lift, lift_univ, univ_umax.{u,v}] at this
no goals
α : Type ?u.234294
β : Type ?u.234297
γ : Type ?u.234300
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
c : Cardinal
this : lift c < univ
⊢ lift c < univ
exact this