Module: Mathlib.Algebra.Category.CoalgCat.Monoidal

Goal state before:
pp: 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✝

Tactic:
;

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✝