Mathlib Reflective: essImage ↔ IsIso unit, via the adjunction's own lemma

For a fully faithful right adjoint R with adj : L ⊣ R, use adj.isIso_unit_app_iff_mem_essImage : IsIso (adj.unit.app Y) ↔ R.essImage Y (Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean). It is dot notation on the adjunction, not a root lemma, so isIso_unit_app_iff_mem_essImage alone gives 'unknown identifier'. The Reflective-file versions (Functor.essImage.unit_isIso) are stated for reflectorAdjunction i, which is not syntactically your adjunction. First rewrite the unit with your own unit_app lemma, then apply the adjunction version. Separate gotcha: variable (G) in before a def that binds its own {G : Type*} makes G explicit for the outer section variable, not for your binder, which leads to baffling 'expected Quot ...' errors at use sites. Put (G : Type*) in the def's own binders instead.