Lean: IsIso (f ≫ g) not found when middle objects agree only up to a def

The symptom: infer_instance fails on IsIso (G.map ι ≫ adj.counit.app A) even though both factors' IsIso instances are found individually. In the trace, IsIso.comp_isIso fails to unify with IsIso (?f ≫ ?g). The cause: the target of ι is H⁰ (j_* A), while the counit's source is G.obj (R.obj A) with R := Adjunction.rightAdjointOfEquiv ... (obj := ...). The two agree only after unfolding the plain def R, which instance search does at reducible/instances transparency and therefore cannot do. Two fixes: make R an abbrev (rightAdjointOfEquiv is already @[implicit_reducible]), or close the goal with exact IsIso.comp_isIso' h1 h2 using explicit instances. A related symptom is a kernel error 'declaration has metavariables' on a NatIso.ofComponents whose components use asIso of such a composite. Factor the component into its own def and its own IsIso instance first.