-- Mathlib/CategoryTheory/EqToHom.lean
theorem ext {F G : C ⥤ D} (h_obj : ∀ X, F.obj X = G.obj X)
    (h_map : ∀ X Y f,
      F.map f = eqToHom (h_obj X) ≫ G.map f ≫ eqToHom (h_obj Y).symm

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map_id✝ : ∀ (X : C), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (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
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
        eqToHom ⋯ ≫ { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯)
    _auto✝
⊢ F_obj = G_obj

Tactic:
ext X

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map_id✝ : ∀ (X : C), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (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
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
        eqToHom ⋯ ≫ { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯)
    _auto✝
X : C
⊢ F_obj X = G_obj X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), { obj := F_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝ }.map (f ≫ g) =
      { obj := F_obj, map := map✝ }.map f ≫ { obj := F_obj, map := map✝ }.map g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
        eqToHom ⋯ ≫ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯)
    _auto✝
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
congr

Result:
case e_toPrefunctor.e_map
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), { obj := F_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝ }.map (f ≫ g) =
      { obj := F_obj, map := map✝ }.map f ≫ { obj := F_obj, map := map✝ }.map g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
        eqToHom ⋯ ≫ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯)
    _auto✝
⊢ map✝¹ = map✝