-- Module: Mathlib.CategoryTheory.Functor.FullyFaithful
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map_1 : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id : ∀ (X : C), map_1 (𝟙 X) = 𝟙 (F_obj X)
map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
inst_3 :
  { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.Faithful
G_obj : D → E
map_2 : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id_1 : ∀ (X : D), map_2 (𝟙 X) = 𝟙 (G_obj X)
map_comp_1 : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map_2 (f ≫ g) = map_2 f ≫ map_2 g
inst_4 :
  { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
        (obj X) =
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.map
        (map f) ≍
      { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }.map f
this : F_obj = G_obj ∘ obj
subst :
  ∀ (map_3 : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y))
    (map_id : ∀ (X : C), map_3 (𝟙 X) = 𝟙 ((G_obj ∘ obj) X))
    (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map_3 (f ≫ g) = map_3 f ≫ map_3 g)
    [{ obj := G_obj ∘ obj, map := @map_3, map_id := map_id, map_comp := @map_comp :
          Functor.{v₁, v₃, u₁, u₃} C E }.Faithful]
    (h_obj :
      ∀ (X : C),
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
            (obj X) =
          { obj := G_obj ∘ obj, map := @map_3, map_id := map_id, map_comp := @map_comp :
                Functor.{v₁, v₃, u₁, u₃} C E }.obj
            X)
    (h_map :
      ∀ {X Y : C} {f : X ⟶ Y},
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.map
            (map f) ≍
          { obj := G_obj ∘ obj, map := @map_3, map_id := map_id, map_comp := @map_comp :
                Functor.{v₁, v₃, u₁, u₃} C E }.map
            f),
    {
        obj := fun (X : C) ↦
          { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 :
                Functor.{v₂, v₃, u₂, u₃} D E }.obj
            ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }.obj X),
        map := fun {X Y : C} (f : X ⟶ Y) ↦
          { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 }.map
            ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ }.map f),
        map_id := ⋯, map_comp := ⋯ } =
      { obj := G_obj ∘ obj, map := @map_3, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
⊢ {
      obj := fun (X : C) ↦
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 : Functor.{v₂, v₃, u₂, u₃} D E }.obj
          ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ : Functor.{v₁, v₂, u₁, u₂} C D }.obj X),
      map := fun {X Y : C} (f : X ⟶ Y) ↦
        { obj := G_obj, map := @map_2, map_id := map_id_1, map_comp := @map_comp_1 }.map
          ({ obj := obj, map := @map, map_id := ⋯, map_comp := ⋯ }.map f),
      map_id := ⋯, map_comp := ⋯ } =
    { obj := F_obj, map := @map_1, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }

Tactic:
subst this