-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
inst_6 : AddMonoid M
inst_7 : AddMonoid N
f : M →+ N
h :
  ∀ (x : M),
    Eq (α := TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
      ((Additive.toMul :
            (a : Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))) →
              TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
          ((((MonoidHom.toAdditiveRight :
                    (a : Multiplicative M →* TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)) →
                      M →+ Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)))
                  (MonoidHom.comp
                    (↑(AlgHom.comp
                            (Algebra.TensorProduct.map (AddMonoidAlgebra.mapDomainAlgHom R R f)
                                (AddMonoidAlgebra.mapDomainAlgHom R R f) :
                              TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R M) →ₐ[R]
                                TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
                            (comulAlgHom R (AddMonoidAlgebra R M) :
                              AddMonoidAlgebra R M →ₐ[R]
                                TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R M)) :
                          AddMonoidAlgebra R M →ₐ[R] TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)) :
                      AddMonoidAlgebra R M →* TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
                    (AddMonoidAlgebra.of R M)) :
                M →+ Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))) :
              (a : M) → Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)))
            x) :
        TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
      ((Additive.toMul :
            (a : Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))) →
              TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
          ((((MonoidHom.toAdditiveRight :
                    (a : Multiplicative M →* TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)) →
                      M →+ Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)))
                  (MonoidHom.comp
                    (↑(AlgHom.comp (comulAlgHom R (AddMonoidAlgebra R N)) (AddMonoidAlgebra.mapDomainAlgHom R R f)) :
                      AddMonoidAlgebra R M →* TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
                    (AddMonoidAlgebra.of R M)) :
                M →+ Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))) :
              (a : M) → Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)))
            x) :
        TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
⊢ Eq (α := AddMonoidAlgebra R M →ₐ[R] TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
    (AlgHom.comp
        (Algebra.TensorProduct.map (AddMonoidAlgebra.mapDomainAlgHom R R f) (AddMonoidAlgebra.mapDomainAlgHom R R f) :
          TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R M) →ₐ[R]
            TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
        (comulAlgHom R (AddMonoidAlgebra R M) :
          AddMonoidAlgebra R M →ₐ[R] TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R M)) :
      AddMonoidAlgebra R M →ₐ[R] TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
    (AlgHom.comp (comulAlgHom R (AddMonoidAlgebra R N)) (AddMonoidAlgebra.mapDomainAlgHom R R f) :
      AddMonoidAlgebra R M →ₐ[R] TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))

Tactic:
ext