Lean: a non-reducible `def X := Abelian.image f` breaks rw on composites

If you define an object as noncomputable def myObj A : C := Abelian.image (h A) and a functor whose obj is definitionally myObj A, then lemmas mixing Abelian.factorThruImage (h A) ≫ F.map f fail. rw [assoc] reports 'did not find (?f ≫ ?g) ≫ ?h' with 'target not type-correct under implicit transparency', because F.map f : myObj A ⟶ myObj B and factorThruImage lands in Abelian.image (h A). Fix: introduce a helper def myMap f : Abelian.image (h A) ⟶ Abelian.image (h B) := F.map f, typed with the unfolded objects, and state the factorization lemmas about it. Statements like Mono (F.map f) then follow from mono_of_mono_fac (myMap_ι f) by defeq. When an IsIso/Mono of a composite is not found even though both factors are, add have := mono_comp _ _ explicitly together with set_option backward.isDefEq.respectTransparency false in.