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

Tactic:
ext : 1