-- 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:
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

Tactic:
ext X Y

Result:
case e_map.h.h
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
X Y : C
⊢ F_map X Y = G_map X Y

Proof state:
case e_map.h.h
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
X Y : C
⊢ F_map X Y = G_map X Y

Tactic:
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₁
inst✝² : EnrichedCategory V C✝
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
X Y : C
⊢ EnrichedCategory.Hom (F.obj X) (F.obj Y) = EnrichedCategory.Hom (G.obj X) (G.obj Y)

Tactic:
rw [h_obj, h_obj]

Result:
no goals