no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
L : C ⥤ D
R : D ⥤ C
inst✝¹ : PreservesMonomorphisms L
adj : L ⊣ R
J : D
inst✝ : Injective J
A x✝ : C
g : A ⟶ R.obj J
f : A ⟶ x✝
im : Mono f
⊢ ↑(Adjunction.homEquiv adj A J).symm
      (f ≫ ↑(Adjunction.homEquiv adj x✝ J) (factorThru (↑(Adjunction.homEquiv adj A J).symm g) (L.map f))) =
    ↑(Adjunction.homEquiv adj A J).symm g
simp