-- Mathlib/CategoryTheory/Enriched/Basic.lean
lemma EnrichedFunctor.ext {C : Type u₁} {D : Type u₂} [EnrichedCategory V C]
    [EnrichedCategory V D] {F G : EnrichedFunctor V C D} (h_obj : ∀ X, F.obj X = G.obj X)
    (h_map : ∀ (X Y : C), F.map X Y ≫ eqToHom (by rw [h_obj, h_obj]) = G.map X Y) : F = G

Proof state:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
h_obj : ∀ (X : C), F.obj X = G.obj X
h_map : ∀ (X Y : C), F.map X Y ≫ eqToHom ⋯ = G.map X Y
⊢ F = G

Tactic:
match F, G with
| mk F_obj F_map _ _, mk G_obj G_map _ _ =>
  obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X
  congr
  ext X Y
  simpa using h_map X Y

Result:
no goals

Proof state:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
F_obj : C → D
F_map : (X Y : C) → EnrichedCategory.Hom X Y ⟶ EnrichedCategory.Hom (F_obj X) (F_obj Y)
map_id✝¹ : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp✝¹ : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_obj : C → D
G_map : (X Y : C) → EnrichedCategory.Hom X Y ⟶ EnrichedCategory.Hom (G_obj X) (G_obj Y)
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (G_obj X)
map_comp✝ : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ G_map Y Z) ≫ eComp V (G_obj X) (G_obj Y) (G_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map X Y ≫ eqToHom ⋯ =
      { obj := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
⊢ { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := G_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X

Result:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
F_obj : C → D
F_map : (X Y : C) → EnrichedCategory.Hom X Y ⟶ EnrichedCategory.Hom (F_obj X) (F_obj Y)
map_id✝¹ : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp✝¹ : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map : (X Y : C) → EnrichedCategory.Hom X Y ⟶ EnrichedCategory.Hom (F_obj X) (F_obj Y)
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp✝ : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map X Y ≫ eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
⊢ { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }

Proof state:
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
F_obj : C → D
F_map : (X Y : C) → EnrichedCategory.Hom X Y ⟶ EnrichedCategory.Hom (F_obj X) (F_obj Y)
map_id✝¹ : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp✝¹ : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map : (X Y : C) → EnrichedCategory.Hom X Y ⟶ EnrichedCategory.Hom (F_obj X) (F_obj Y)
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp✝ : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map X Y ≫ eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
⊢ { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
congr

Result:
case e_map
V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
F_obj : C → D
F_map : (X Y : C) → EnrichedCategory.Hom X Y ⟶ EnrichedCategory.Hom (F_obj X) (F_obj Y)
map_id✝¹ : ∀ (X : C), eId V X ≫ F_map X X = eId V (F_obj X)
map_comp✝¹ : ∀ (X Y Z : C), eComp V X Y Z ≫ F_map X Z = (F_map X Y ⊗ F_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
G_map : (X Y : C) → EnrichedCategory.Hom X Y ⟶ EnrichedCategory.Hom (F_obj X) (F_obj Y)
map_id✝ : ∀ (X : C), eId V X ≫ G_map X X = eId V (F_obj X)
map_comp✝ : ∀ (X Y Z : C), eComp V X Y Z ≫ G_map X Z = (G_map X Y ⊗ G_map Y Z) ≫ eComp V (F_obj X) (F_obj Y) (F_obj Z)
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C),
    { obj := F_obj, map := F_map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map X Y ≫ eqToHom ⋯ =
      { obj := F_obj, map := G_map, map_id := map_id✝, map_comp := map_comp✝ }.map X Y
⊢ F_map = G_map