-- 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
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)))
                                ((𝟙_ (CoalgCat R)) (𝒞 := category))))))) :
                    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 M)))))) :
                    Type u))
                (CoalgHom.toLinearMap (Hom.toCoalgHom' (Iso.hom (λ_ (of R M))))) :
              (a : R) →
                (↑(Opposite.unop
                        (Opposite.unop
                            ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                              ((comonEquivalence R).symm.inverse.obj (of R M)))).X) :
                    Type u) →ₗ[R]
                  (↑(of R M).toModuleCat : Type u))
            1 :
          (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)) →
            (↑(of R M).toModuleCat : Type u))
        x :
      (↑(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)))
                                ((𝟙_ (CoalgCat R)) (𝒞 := category))))))) :
                    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 M)))))) :
                    Type u))
                (↑(TensorProduct.lid R M) : TensorProduct R R M →ₗ[R] M) :
              (a : R) →
                (↑(Opposite.unop
                        (Opposite.unop
                            ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                              ((comonEquivalence R).symm.inverse.obj (of R M)))).X) :
                    Type u) →ₗ[R]
                  (↑(of R M).toModuleCat : Type u))
            1 :
          (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)) →
            (↑(of R M).toModuleCat : Type u))
        x :
      (↑(toModuleCat (of R M)) : Type u))

Tactic:
rfl