Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : CoalgCat R
⊢ (TensorProduct.mk R ↑X.toModuleCat ↑Y.toModuleCat).compr₂ₛₗ
      ((TensorProduct.mk R ↑(X ⊗ Y).toModuleCat ↑Z.toModuleCat).compr₂ₛₗ
        (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (α_ X Y Z).hom))) =
    (TensorProduct.mk R ↑X.toModuleCat ↑Y.toModuleCat).compr₂ₛₗ
      ((TensorProduct.mk R ↑(X ⊗ Y).toModuleCat ↑Z.toModuleCat).compr₂ₛₗ
        (ModuleCat.Hom.hom
          (((Iso.refl
                    ((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y) ⊗
                      (forget₂ (CoalgCat R) (ModuleCat R)).obj Z)).symm ≪≫
                ((Iso.refl
                      ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj Y)).symm ⊗ᵢ
                  Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj Z))) ≪≫
              α_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X) ((forget₂ (CoalgCat R) (ModuleCat R)).obj Y)
                  ((forget₂ (CoalgCat R) (ModuleCat R)).obj Z) ≪≫
                (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X) ⊗ᵢ
                    Iso.refl
                      ((forget₂ (CoalgCat R) (ModuleCat R)).obj Y ⊗ (forget₂ (CoalgCat R) (ModuleCat R)).obj Z)) ≪≫
                  Iso.refl
                    ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗
                      (forget₂ (CoalgCat R) (ModuleCat R)).obj (Y ⊗ Z))).hom))

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : CoalgCat R
x✝² : ↑X.toModuleCat
x✝¹ : ↑Y.toModuleCat
x✝ : ↑Z.toModuleCat
⊢ ((((TensorProduct.mk R ↑X.toModuleCat ↑Y.toModuleCat).compr₂ₛₗ
            ((TensorProduct.mk R ↑(X ⊗ Y).toModuleCat ↑Z.toModuleCat).compr₂ₛₗ
              (ModuleCat.Hom.hom ((forget₂ (CoalgCat R) (ModuleCat R)).map (α_ X Y Z).hom))))
          x✝²)
        x✝¹)
      x✝ =
    ((((TensorProduct.mk R ↑X.toModuleCat ↑Y.toModuleCat).compr₂ₛₗ
            ((TensorProduct.mk R ↑(X ⊗ Y).toModuleCat ↑Z.toModuleCat).compr₂ₛₗ
              (ModuleCat.Hom.hom
                (((Iso.refl
                          ((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y) ⊗
                            (forget₂ (CoalgCat R) (ModuleCat R)).obj Z)).symm ≪≫
                      ((Iso.refl
                            ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗
                              (forget₂ (CoalgCat R) (ModuleCat R)).obj Y)).symm ⊗ᵢ
                        Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj Z))) ≪≫
                    α_ ((forget₂ (CoalgCat R) (ModuleCat R)).obj X) ((forget₂ (CoalgCat R) (ModuleCat R)).obj Y)
                        ((forget₂ (CoalgCat R) (ModuleCat R)).obj Z) ≪≫
                      (Iso.refl ((forget₂ (CoalgCat R) (ModuleCat R)).obj X) ⊗ᵢ
                          Iso.refl
                            ((forget₂ (CoalgCat R) (ModuleCat R)).obj Y ⊗
                              (forget₂ (CoalgCat R) (ModuleCat R)).obj Z)) ≪≫
                        Iso.refl
                          ((forget₂ (CoalgCat R) (ModuleCat R)).obj X ⊗
                            (forget₂ (CoalgCat R) (ModuleCat R)).obj (Y ⊗ Z))).hom)))
          x✝²)
        x✝¹)
      x✝