Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
inst✝¹ : { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful
G_obj : D → E
map✝ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : D), map✝ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
inst✝ : { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj (obj X) =
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map (map f) ≍
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f
⊢ {
      obj := fun X ↦
        { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj
          ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.obj X),
      map := fun {X Y} f ↦
        { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map
          ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map f),
      map_id := ⋯, map_comp := ⋯ } =
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }

Tactic:
have : F_obj = G_obj ∘ obj := (funext h_obj).symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
inst✝¹ : { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful
G_obj : D → E
map✝ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : D), map✝ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝ : ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
inst✝ : { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful
h_obj :
  ∀ (X : C),
    { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj (obj X) =
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map (map f) ≍
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f
this : F_obj = G_obj ∘ obj
⊢ {
      obj := fun X ↦
        { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj
          ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.obj X),
      map := fun {X Y} f ↦
        { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map
          ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map f),
      map_id := ⋯, map_comp := ⋯ } =
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }