-- 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
h :
  ∀
    (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))
⊢ Eq (α :=
    (↑(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) →ₗ[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 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))
    (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)))))))
    (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))))

Tactic:
ext