-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C_1 : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C_1
C : Type v
inst_3 : EnrichedCategory (Type v) C
D : Type v
inst_4 : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ :
  Functor.obj
    (Functor.obj yoneda
      (Quiver.Hom (V := C ⥤ D)
        ((enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) F : C ⥤ D)
        ((enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) G : C ⥤ D)))
    α
X Y : C
h :
  ∀ (x : Sigma.fst (β := fun (X : Type v) ↦ HalfBraiding X) (Functor.obj (Center.ofBraided (Type v)) (unop α)))
    (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              (HalfBraiding.β
                (Sigma.snd (β := fun (X : Type v) ↦ HalfBraiding X) (Functor.obj (Center.ofBraided (Type v)) (unop α)))
                (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y)) ≫
            (F.map X Y ⊗ₘ
                ↾fun
                    (x :
                      Sigma.fst (β := fun (X : Type v) ↦ HalfBraiding X)
                        (Functor.obj (Center.ofBraided (Type v)) (unop α))) ↦
                  NatTrans.app
                    ((TypeCat.Hom.hom σ :
                        (a : unop α) →
                          (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) F ⟶
                            (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) G)
                      x)
                    Y) ≫
              eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y)))
        (x, f) =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((↾fun
                  (x :
                    Sigma.fst (β := fun (X : Type v) ↦ HalfBraiding X)
                      (Functor.obj (Center.ofBraided (Type v)) (unop α))) ↦
                NatTrans.app
                  ((TypeCat.Hom.hom σ :
                      (a : unop α) →
                        (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) F ⟶
                          (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) G)
                    x)
                  X) ⊗ₘ
              G.map X Y) ≫
            eComp (Type v) (F.obj X) (G.obj X) (G.obj Y)))
        (x, f)
⊢ Eq (α :=
    tensorObj (𝒞 := types)
        (Sigma.fst (β := fun (X : Type v) ↦ HalfBraiding X) (Functor.obj (Center.ofBraided (Type v)) (unop α)))
        (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y) ⟶
      @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ (F.obj X) (G.obj Y))
    (Iso.hom
        (HalfBraiding.β
          (Sigma.snd (β := fun (X : Type v) ↦ HalfBraiding X) (Functor.obj (Center.ofBraided (Type v)) (unop α)))
          (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y)) ≫
      (F.map X Y ⊗ₘ
          ↾fun
              (x :
                Sigma.fst (β := fun (X : Type v) ↦ HalfBraiding X) (Functor.obj (Center.ofBraided (Type v)) (unop α))) ↦
            NatTrans.app
              ((TypeCat.Hom.hom σ :
                  (a : unop α) →
                    (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) F ⟶
                      (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) G)
                x)
              Y) ≫
        eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y))
    (((↾fun
            (x :
              Sigma.fst (β := fun (X : Type v) ↦ HalfBraiding X) (Functor.obj (Center.ofBraided (Type v)) (unop α))) ↦
          NatTrans.app
            ((TypeCat.Hom.hom σ :
                (a : unop α) →
                  (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) F ⟶
                    (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) G)
              x)
            X) ⊗ₘ
        G.map X Y) ≫
      eComp (Type v) (F.obj X) (G.obj X) (G.obj Y))

Tactic:
ext ⟨x, f⟩