-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem rightUnitor_hom_toLinearMap :
    (ρ_ (CoalgebraCat.of R M)).hom.1.toLinearMap = (TensorProduct.rid R M).toLinearMap :=
  TensorProduct.ext <| by ext; rfl

Proof state:
case h.h
R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgebraCat R))))).X)).compr₂
          (ρ_ (of R M)).hom.toCoalgHom'.toLinearMap)
        x✝)
      1 =
    (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgebraCat R))))).X)).compr₂
          ↑(TensorProduct.rid R M))
        x✝)
      1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
⊢ (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgebraCat R))))).X)).compr₂
      (ρ_ (of R M)).hom.toCoalgHom'.toLinearMap =
    (TensorProduct.mk R
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
          ↑(Opposite.unop
              (Opposite.unop
                  ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                    ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgebraCat R))))).X)).compr₂
      ↑(TensorProduct.rid R M)

Tactic:
ext

Result:
case h.h
R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgebraCat R))))).X)).compr₂
          (ρ_ (of R M)).hom.toCoalgHom'.toLinearMap)
        x✝)
      1 =
    (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon_.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgebraCat R))))).X)).compr₂
          ↑(TensorProduct.rid R M))
        x✝)
      1