α✝ : Type ?u.236087
β : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ Small α ↔ ∃ c', lift (#α) = lift c'
α✝ : Type ?u.236087
β : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ Small α ↔ lift (#α) < univ
rw [lt_univ']
case mp
α✝ : Type ?u.236087
β : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ Small α → ∃ c', lift (#α) = lift c'

case mpr
α✝ : Type ?u.236087
β : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ (∃ c', lift (#α) = lift c') → Small α
α✝ : Type ?u.236087
β : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ Small α ↔ ∃ c', lift (#α) = lift c'
constructor
case mp.mk.intro
α✝ : Type ?u.236087
β✝ : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
e : Nonempty (α ≃ β)
⊢ ∃ c', lift (#α) = lift c'
case mp
α✝ : Type ?u.236087
β : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ Small α → ∃ c', lift (#α) = lift c'
rintro ⟨β, e⟩
no goals
case mp.mk.intro
α✝ : Type ?u.236087
β✝ : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
α : Type u
β : Type v
e : Nonempty (α ≃ β)
⊢ ∃ c', lift (#α) = lift c'
exact ⟨#β, lift_mk_eq.{u, _, v + 1}.2 e⟩
case mpr.intro
α✝ : Type ?u.236087
β : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
c : Cardinal
hc : lift (#α) = lift c
⊢ Small α
case mpr
α✝ : Type ?u.236087
β : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
⊢ (∃ c', lift (#α) = lift c') → Small α
rintro ⟨c, hc⟩
no goals
case mpr.intro
α✝ : Type ?u.236087
β : Type ?u.236090
γ : Type ?u.236093
r : α✝ → α✝ → Prop
s : β → β → Prop
t : γ → γ → Prop
α : Type u
c : Cardinal
hc : lift (#α) = lift c
⊢ Small α
exact ⟨⟨c.out, lift_mk_eq.{u, _, v + 1}.1 (hc.trans (congr rfl c.mk_out.symm))⟩⟩