-- 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
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : Type vᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      (enrichedNatTransYoneda F G).obj X ⟶
        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)))
          Y)
      ((enrichedNatTransYoneda F G).map f ≫
        Iso.hom
          ((fun (α : Type vᵒᵖ) ↦
              {
                hom :=
                  ↾fun (σ : (enrichedNatTransYoneda F G).obj α) ↦
                    ↾fun (x : unop α) ↦
                      {
                        app := fun (X : C) ↦
                          (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app X) :
                              (a : (fun (X : Type v) ↦ X) ((Center.ofBraided (Type v)).obj (unop α)).fst) →
                                (fun (X : Type v) ↦ X) (F.obj X ⟶[Type v] G.obj X))
                            x,
                        naturality := ⋯ },
                inv :=
                  ↾fun
                      (σ :
                        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)))
                          α) ↦
                    {
                      app := fun (X : C) ↦
                        ↾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,
                      naturality := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                (enrichedNatTransYoneda F G).obj α ≅
                  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)))
                    α })
            Y))
      (Iso.hom
          ((fun (α : Type vᵒᵖ) ↦
              {
                hom :=
                  ↾fun (σ : (enrichedNatTransYoneda F G).obj α) ↦
                    ↾fun (x : unop α) ↦
                      {
                        app := fun (X : C) ↦
                          (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app X) :
                              (a : (fun (X : Type v) ↦ X) ((Center.ofBraided (Type v)).obj (unop α)).fst) →
                                (fun (X : Type v) ↦ X) (F.obj X ⟶[Type v] G.obj X))
                            x,
                        naturality := ⋯ },
                inv :=
                  ↾fun
                      (σ :
                        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)))
                          α) ↦
                    {
                      app := fun (X : C) ↦
                        ↾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,
                      naturality := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                (enrichedNatTransYoneda F G).obj α ≅
                  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) ≫
        Functor.map
          (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)))
          f)
⊢ ∀ {X Y : Type vᵒᵖ} (f : X ⟶ Y),
    Eq (α :=
      (enrichedNatTransYoneda F G).obj X ⟶
        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)))
          Y)
      ((enrichedNatTransYoneda F G).map f ≫
        Iso.hom
          ((fun (α : Type vᵒᵖ) ↦
              {
                hom :=
                  ↾fun (σ : (enrichedNatTransYoneda F G).obj α) ↦
                    ↾fun (x : unop α) ↦
                      {
                        app := fun (X : C) ↦
                          (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app X) :
                              (a : (fun (X : Type v) ↦ X) ((Center.ofBraided (Type v)).obj (unop α)).fst) →
                                (fun (X : Type v) ↦ X) (F.obj X ⟶[Type v] G.obj X))
                            x,
                        naturality := ⋯ },
                inv :=
                  ↾fun
                      (σ :
                        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)))
                          α) ↦
                    {
                      app := fun (X : C) ↦
                        ↾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,
                      naturality := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                (enrichedNatTransYoneda F G).obj α ≅
                  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)))
                    α })
            Y))
      (Iso.hom
          ((fun (α : Type vᵒᵖ) ↦
              {
                hom :=
                  ↾fun (σ : (enrichedNatTransYoneda F G).obj α) ↦
                    ↾fun (x : unop α) ↦
                      {
                        app := fun (X : C) ↦
                          (ConcreteCategory.hom (FC := TypeCat.Fun) (σ.app X) :
                              (a : (fun (X : Type v) ↦ X) ((Center.ofBraided (Type v)).obj (unop α)).fst) →
                                (fun (X : Type v) ↦ X) (F.obj X ⟶[Type v] G.obj X))
                            x,
                        naturality := ⋯ },
                inv :=
                  ↾fun
                      (σ :
                        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)))
                          α) ↦
                    {
                      app := fun (X : C) ↦
                        ↾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,
                      naturality := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                (enrichedNatTransYoneda F G).obj α ≅
                  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) ≫
        Functor.map
          (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)))
          f)

Tactic:
cat_disch