-- Module: Mathlib.Probability.Kernel.Category.SFinKer
Goal:
X Y Z : SFinKer
h :
  Eq (α :=
    Kernel
      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X
          (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y Z)).carrier
      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory)
          (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X) Y).carrier)
    (Hom.hom
      (Iso.inv (α_ X Y Z) ≫
        Iso.hom
            {
              hom :=
                { hom := Kernel.swap (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier Z.carrier,
                  property := ⋯ },
              inv :=
                { hom := Kernel.swap Z.carrier (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier,
                  property := ⋯ },
              hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
          Iso.inv (α_ Z X Y)))
    (Hom.hom
      (X ◁
          Iso.hom
            { hom := { hom := Kernel.swap Y.carrier Z.carrier, property := ⋯ },
              inv := { hom := Kernel.swap Z.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
        Iso.inv (α_ X Z Y) ≫
          Iso.hom
              {
                hom :=
                  { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ :
                    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Z).Hom
                      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X) },
                inv :=
                  { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ :
                    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X).Hom
                      (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Z) },
                hom_inv_id := ⋯, inv_hom_id := ⋯ :
                MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Z ≅
                  MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X } ▷
            Y))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X
        (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Y Z) ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory)
        (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X) Y)
    (Iso.inv (α_ X Y Z) ≫
      Iso.hom
          {
            hom :=
              { hom := Kernel.swap (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier Z.carrier,
                property := ⋯ },
            inv :=
              { hom := Kernel.swap Z.carrier (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier,
                property := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
        Iso.inv (α_ Z X Y))
    (X ◁
        Iso.hom
          { hom := { hom := Kernel.swap Y.carrier Z.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Z.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      Iso.inv (α_ X Z Y) ≫
        Iso.hom
            {
              hom :=
                { hom := Kernel.swap X.carrier Z.carrier, property := ⋯ :
                  (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Z).Hom
                    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X) },
              inv :=
                { hom := Kernel.swap Z.carrier X.carrier, property := ⋯ :
                  (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X).Hom
                    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Z) },
              hom_inv_id := ⋯, inv_hom_id := ⋯ :
              MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Z ≅
                MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X } ▷
          Y)

Tactic:
ext : 1