-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Coalgebra R M
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)),
    Eq (α := (↑(toModuleCat (of R M)) : 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)))
                                    ((𝟙_ (CoalgCat R)) (𝒞 := category))))))) :
                        Type u))
                    (CoalgHom.toLinearMap (Hom.toCoalgHom' (Iso.hom (ρ_ (of R M))))) :
                  (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 (𝟙_ (CoalgCat R))))).X) :
                        Type u) →ₗ[R]
                      (↑(of R M).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)))
                              ((𝟙_ (CoalgCat R)) (𝒞 := category))))))) :
                  Type u) →ₗ[R]
                (↑(toModuleCat (of R M)) : Type u)) :
            (a : R) → (↑(of R M).toModuleCat : Type u))
          1 :
        (↑(toModuleCat (of R M)) : 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)))
                                    ((𝟙_ (CoalgCat R)) (𝒞 := category))))))) :
                        Type u))
                    (↑(TensorProduct.rid R M) : TensorProduct R M R →ₗ[R] M) :
                  (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 (𝟙_ (CoalgCat R))))).X) :
                        Type u) →ₗ[R]
                      (↑(of R M).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)))
                              ((𝟙_ (CoalgCat R)) (𝒞 := category))))))) :
                  Type u) →ₗ[R]
                (↑(toModuleCat (of R M)) : Type u)) :
            (a : R) → (↑(of R M).toModuleCat : Type u))
          1 :
        (↑(toModuleCat (of R M)) : 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)))
                      ((𝟙_ (CoalgCat R)) (𝒞 := category))))))) :
          Type u) →ₗ[R]
        (↑(toModuleCat (of R M)) : 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)))
                      ((𝟙_ (CoalgCat R)) (𝒞 := category))))))) :
          Type u))
      (CoalgHom.toLinearMap (Hom.toCoalgHom' (Iso.hom (ρ_ (of R M))))))
    (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)))
                      ((𝟙_ (CoalgCat R)) (𝒞 := category))))))) :
          Type u))
      (↑(TensorProduct.rid R M) : TensorProduct R M R →ₗ[R] M))

Tactic:
ext