-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
theorem Faithful.div_comp (F : C ⥤ E) [F.Faithful] (G : D ⥤ E) [G.Faithful] (obj : C → D)
    (h_obj : ∀ X, G.obj (obj X) = F.obj X) (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) :
    Faithful.div F G obj @h_obj @map @h_map ⋙ G = F

Proof state:
case mk.mk.mk.mk
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)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g
inst✝¹ : { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g
inst✝ : { obj := G_obj ∘ 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 := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ({ obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map (map f))
      ({ obj := G_obj ∘ 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 := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
congr

Result:
case mk.mk.mk.mk.e_toPrefunctor.e_map
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)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g
inst✝¹ : { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g
inst✝ : { obj := G_obj ∘ 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 := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ({ obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map (map f))
      ({ obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f)
⊢ (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✝

Proof state:
case mk.mk.mk.mk.e_toPrefunctor.e_map
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)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g
inst✝¹ : { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g
inst✝ : { obj := G_obj ∘ 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 := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map✝ :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ({ obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map (map f))
      ({ obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, map✝¹ (map f) = map✝ f
⊢ (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✝

Tactic:
ext

Result:
case mk.mk.mk.mk.e_toPrefunctor.e_map.h.h.h
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)
G_obj : D → E
map✝¹ : {X Y : D} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : D), { obj := G_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : D} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := G_obj, map := map✝¹ }.map f ≫ { obj := G_obj, map := map✝¹ }.map g
inst✝¹ : { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.Faithful
map✝ : {X Y : C} → (X ⟶ Y) → ((G_obj ∘ obj) X ⟶ (G_obj ∘ obj) Y)
map_id✝ : ∀ (X : C), { obj := G_obj ∘ obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj ∘ obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj ∘ obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj ∘ obj, map := map✝ }.map f ≫ { obj := G_obj ∘ obj, map := map✝ }.map g
inst✝ : { obj := G_obj ∘ 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 := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map✝ :
  ∀ {X Y : C} {f : X ⟶ Y},
    HEq ({ obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map (map f))
      ({ obj := G_obj ∘ obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, map✝¹ (map f) = map✝ f
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ { obj := G_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map
      ({ obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }.map x✝) =
    map✝ x✝