-- Lean 4 proof step from Mathlib.Probability.Kernel.Category.SFinKer (goal)
Goal:
X Y Z : SFinKer
⊢ 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)
have 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 := sorry },
            inv :=
              { hom := Kernel.swap Z.carrier (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Y).carrier,
                property := sorry },
            hom_inv_id := sorry, inv_hom_id := sorry } ≫
        Iso.inv (α_ Z X Y)))
  (Hom.hom
    (X ◁
        Iso.hom
          { hom := { hom := Kernel.swap Y.carrier Z.carrier, property := sorry },
            inv := { hom := Kernel.swap Z.carrier Y.carrier, property := sorry }, hom_inv_id := sorry, inv_hom_id := sorry } ≫
      Iso.inv (α_ X Z Y) ≫
        Iso.hom
            {
              hom :=
                { hom := Kernel.swap X.carrier Z.carrier, property := sorry :
                  (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Z).Hom
                    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X) },
              inv :=
                { hom := Kernel.swap Z.carrier X.carrier, property := sorry :
                  (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X).Hom
                    (MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Z) },
              hom_inv_id := sorry, inv_hom_id := sorry :
              MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) X Z ≅
                MonoidalCategoryStruct.tensorObj (𝒞 := instLargeCategory) Z X } ▷
          Y))
Tactic: ext : 1