-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
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
⊢ 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))
have 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)
Tactic: ext ⟨x, f⟩