-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N P : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Coalgebra R M
inst_8 : Coalgebra R N
inst_9 : Coalgebra R P
x :
  (↑(Opposite.unop
        (Mon.X
          (Opposite.unop
            (Functor.obj
              (Equivalence.inverse (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
              (Functor.obj (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R))) (of R M)))))) :
    Type u)
x_1 :
  (↑(Opposite.unop
        (Mon.X
          (Opposite.unop
            (Functor.obj
              (Equivalence.inverse (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
              (Functor.obj (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R))) (of R N)))))) :
    Type u)
x_2 :
  (↑(Opposite.unop
        (Mon.X
          (Opposite.unop
            (Functor.obj
              (Equivalence.inverse (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
              (Functor.obj (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R))) (of R P)))))) :
    Type u)
⊢ Eq (α := (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u))
    ((((((LinearMap.compr₂ₛₗ
                        (TensorProduct.mk R
                          (↑(Opposite.unop
                                (Mon.X
                                  (Opposite.unop
                                    (Functor.obj
                                      (Equivalence.inverse
                                        (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                      (Functor.obj
                                        (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                        (of R M)))))) :
                            Type u)
                          (↑(Opposite.unop
                                (Mon.X
                                  (Opposite.unop
                                    (Functor.obj
                                      (Equivalence.inverse
                                        (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                      (Functor.obj
                                        (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                        (of R N)))))) :
                            Type u))
                        (LinearMap.compr₂ₛₗ
                          (TensorProduct.mk R
                            (↑(Opposite.unop
                                  (Mon.X
                                    (Opposite.unop
                                      (Functor.obj
                                        (Equivalence.inverse
                                          (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                        (Functor.obj
                                          (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                          (tensorObj (𝒞 := category) (of R M) (of R N))))))) :
                              Type u)
                            (↑(Opposite.unop
                                  (Mon.X
                                    (Opposite.unop
                                      (Functor.obj
                                        (Equivalence.inverse
                                          (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                        (Functor.obj
                                          (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                          (of R P)))))) :
                              Type u))
                          (CoalgHom.toLinearMap (Hom.toCoalgHom' (Iso.hom (α_ (of R M) (of R N) (of R P)))))) :
                      (a :
                          (↑(Opposite.unop
                                (Opposite.unop
                                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                      ((comonEquivalence R).symm.inverse.obj (of R M)))).X) :
                            Type u)) →
                        (↑(Opposite.unop
                                (Opposite.unop
                                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                      ((comonEquivalence R).symm.inverse.obj (of R N)))).X) :
                            Type u) →ₗ[R]
                          (↑(Opposite.unop
                                  (Opposite.unop
                                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                        ((comonEquivalence R).symm.inverse.obj (of R P)))).X) :
                              Type u) →ₗ[R]
                            (↑(of R M ⊗ of R N ⊗ of R P).toModuleCat : Type u))
                    x :
                  (↑(Opposite.unop
                          (Mon.X
                            (Opposite.unop
                              (Functor.obj
                                (Equivalence.inverse
                                  (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                (Functor.obj
                                  (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                  (of R N)))))) :
                      Type u) →ₗ[R]
                    (↑(Opposite.unop
                            (Mon.X
                              (Opposite.unop
                                (Functor.obj
                                  (Equivalence.inverse
                                    (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                  (Functor.obj
                                    (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                    (of R P)))))) :
                        Type u) →ₗ[R]
                      (↑(toModuleCat
                            (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) :
                        Type u)) :
                (a :
                    (↑(Opposite.unop
                          (Opposite.unop
                              ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                ((comonEquivalence R).symm.inverse.obj (of R N)))).X) :
                      Type u)) →
                  (↑(Opposite.unop
                          (Opposite.unop
                              ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                ((comonEquivalence R).symm.inverse.obj (of R P)))).X) :
                      Type u) →ₗ[R]
                    (↑(of R M ⊗ of R N ⊗ of R P).toModuleCat : Type u))
              x_1 :
            (↑(Opposite.unop
                    (Mon.X
                      (Opposite.unop
                        (Functor.obj
                          (Equivalence.inverse
                            (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                          (Functor.obj (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                            (of R P)))))) :
                Type u) →ₗ[R]
              (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) :
                Type u)) :
          (a :
              (↑(Opposite.unop
                    (Opposite.unop
                        ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                          ((comonEquivalence R).symm.inverse.obj (of R P)))).X) :
                Type u)) →
            (↑(of R M ⊗ of R N ⊗ of R P).toModuleCat : Type u))
        x_2 :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u))
    ((((((LinearMap.compr₂ₛₗ
                        (TensorProduct.mk R
                          (↑(Opposite.unop
                                (Mon.X
                                  (Opposite.unop
                                    (Functor.obj
                                      (Equivalence.inverse
                                        (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                      (Functor.obj
                                        (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                        (of R M)))))) :
                            Type u)
                          (↑(Opposite.unop
                                (Mon.X
                                  (Opposite.unop
                                    (Functor.obj
                                      (Equivalence.inverse
                                        (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                      (Functor.obj
                                        (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                        (of R N)))))) :
                            Type u))
                        (LinearMap.compr₂ₛₗ
                          (TensorProduct.mk R
                            (↑(Opposite.unop
                                  (Mon.X
                                    (Opposite.unop
                                      (Functor.obj
                                        (Equivalence.inverse
                                          (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                        (Functor.obj
                                          (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                          (tensorObj (𝒞 := category) (of R M) (of R N))))))) :
                              Type u)
                            (↑(Opposite.unop
                                  (Mon.X
                                    (Opposite.unop
                                      (Functor.obj
                                        (Equivalence.inverse
                                          (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                        (Functor.obj
                                          (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                          (of R P)))))) :
                              Type u))
                          (↑(TensorProduct.assoc R M N P) :
                            TensorProduct R (TensorProduct R M N) P →ₗ[R] TensorProduct R M (TensorProduct R N P))) :
                      (a :
                          (↑(Opposite.unop
                                (Opposite.unop
                                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                      ((comonEquivalence R).symm.inverse.obj (of R M)))).X) :
                            Type u)) →
                        (↑(Opposite.unop
                                (Opposite.unop
                                    ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                      ((comonEquivalence R).symm.inverse.obj (of R N)))).X) :
                            Type u) →ₗ[R]
                          (↑(Opposite.unop
                                  (Opposite.unop
                                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                        ((comonEquivalence R).symm.inverse.obj (of R P)))).X) :
                              Type u) →ₗ[R]
                            (↑(of R M ⊗ of R N ⊗ of R P).toModuleCat : Type u))
                    x :
                  (↑(Opposite.unop
                          (Mon.X
                            (Opposite.unop
                              (Functor.obj
                                (Equivalence.inverse
                                  (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                (Functor.obj
                                  (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                  (of R N)))))) :
                      Type u) →ₗ[R]
                    (↑(Opposite.unop
                            (Mon.X
                              (Opposite.unop
                                (Functor.obj
                                  (Equivalence.inverse
                                    (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                                  (Functor.obj
                                    (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                                    (of R P)))))) :
                        Type u) →ₗ[R]
                      (↑(toModuleCat
                            (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) :
                        Type u)) :
                (a :
                    (↑(Opposite.unop
                          (Opposite.unop
                              ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                ((comonEquivalence R).symm.inverse.obj (of R N)))).X) :
                      Type u)) →
                  (↑(Opposite.unop
                          (Opposite.unop
                              ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                                ((comonEquivalence R).symm.inverse.obj (of R P)))).X) :
                      Type u) →ₗ[R]
                    (↑(of R M ⊗ of R N ⊗ of R P).toModuleCat : Type u))
              x_1 :
            (↑(Opposite.unop
                    (Mon.X
                      (Opposite.unop
                        (Functor.obj
                          (Equivalence.inverse
                            (CategoryTheory.Equivalence.symm (Comon.Comon_EquivMon_OpOp (ModuleCat R))))
                          (Functor.obj (Equivalence.inverse (CategoryTheory.Equivalence.symm (comonEquivalence R)))
                            (of R P)))))) :
                Type u) →ₗ[R]
              (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) :
                Type u)) :
          (a :
              (↑(Opposite.unop
                    (Opposite.unop
                        ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                          ((comonEquivalence R).symm.inverse.obj (of R P)))).X) :
                Type u)) →
            (↑(of R M ⊗ of R N ⊗ of R P).toModuleCat : Type u))
        x_2 :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u))

Tactic:
rfl