-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
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
⊢ 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))))
have 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))
Tactic: ext