-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.MonoidAlgebra (goal)
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
⊢ 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))
have 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))
Tactic: ext