[GOAL]
w : EssSurj uliftFunctor.{u, v}
a : Type (max u v)
⊢ Small.{v, max u v} a
[PROOFSTEP]
obtain ⟨a', ⟨m⟩⟩ := w.mem_essImage a
[GOAL]
case intro.intro
w : EssSurj uliftFunctor.{u, v}
a : Type (max u v)
a' : Type v
m : uliftFunctor.{u, v}.obj a' ≅ a
⊢ Small.{v, max u v} a
[PROOFSTEP]
exact ⟨a', ⟨(Iso.toEquiv m).symm.trans Equiv.ulift⟩⟩
