-- Module: Mathlib.CategoryTheory.Adjunction.Restrict
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
iC : Functor.{v₁, v₃, u₁, u₃} C C'
iD : Functor.{v₂, v₄, u₂, u₄} D D'
L' : Functor.{v₃, v₄, u₃, u₄} C' D'
R' : Functor.{v₄, v₃, u₄, u₃} D' C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : Functor.{v₁, v₂, u₁, u₂} C D
R : Functor.{v₂, v₁, u₂, u₁} D C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ R.obj Y
apply :
  Eq (α := iD.obj (L.obj X') ⟶ iD.obj Y)
    (iD.map
      (((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                    ((comm1.symm.app X').homCongr (Iso.refl (iD.obj Y))))
                  (adj.homEquiv (iC.obj X') (iD.obj Y)))
                (Iso.homCongr (Iso.refl (iC.obj X')) (comm2.app Y)))
              (Equiv.symm hiC.homEquiv)).symm :
          (a : X' ⟶ R.obj Y) → L.obj X' ⟶ Y)
        (f ≫ g)))
    (iD.map
      (L.map f ≫
        ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                    (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                      ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
                    (adj.homEquiv (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (Equiv.symm hiC.homEquiv)).symm :
            (a : X ⟶ R.obj Y) → L.obj X ⟶ Y)
          g))
⊢ Eq.{v₂ + 1} (α := L.obj X' ⟶ Y)
    (((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                    ((comm1.symm.app X').homCongr (Iso.refl (iD.obj Y))))
                  (adj.homEquiv (iC.obj X') (iD.obj Y)))
                (Iso.homCongr (Iso.refl (iC.obj X')) (comm2.app Y)))
              (Equiv.symm hiC.homEquiv)).symm :
          (a : X' ⟶ R.obj Y) → L.obj X' ⟶ Y)
        (f ≫ g) :
      L.obj X' ⟶ Y)
    (L.map f ≫
        ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                  (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                    (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) hiD.homEquiv
                      ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
                    (adj.homEquiv (iC.obj X) (iD.obj Y)))
                  (Iso.homCongr (Iso.refl (iC.obj X)) (comm2.app Y)))
                (Equiv.symm hiC.homEquiv)).symm :
            (a : X ⟶ R.obj Y) → L.obj X ⟶ Y)
          g :
      L.obj X' ⟶ Y)

Tactic:
apply hiD.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective