-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FullyFaithful (goal)
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
⊢ {
      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 }
have 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 := sorry, map_comp := sorry : 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 := sorry, map_comp := sorry }.map f),
      map_id := sorry, map_comp := sorry } =
    { obj := G_obj ∘ obj, map := @map_3, map_id := map_id, map_comp := @map_comp : Functor.{v₁, v₃, u₁, u₃} C E }
Tactic: subst this
Cleared hypotheses: F_obj, map_1, map_id, map_comp, inst_3, h_obj, h_map, this