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