-- Module: Mathlib.RingTheory.Flat.Equalizer
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f g : N →ₗ[R] P
x y : M
x_1 : ↥f.ker
⊢ Eq (α := M ⊗[R] N)
    (↑(({
              toFun := fun (a : ↥f.ker) ↦
                Subtype.mk (p := fun (x : M ⊗[R] N) ↦
                  Membership.mem (γ := Submodule S (M ⊗[R] N))
                    (ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
                      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                          (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                        f))
                    x)
                  ((x + y) ⊗ₜ[R] (↑a : N)) ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : ↥f.ker) → ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          x_1) :
      M ⊗[R] N)
    (↑((HAdd.hAdd (α :=
              ↥f.ker →ₗ[R]
                ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
                    (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                        (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                      f)))
              {
                toFun := fun (a : ↥f.ker) ↦
                  Subtype.mk (p := fun (x : M ⊗[R] N) ↦
                    Membership.mem (γ := Submodule S (M ⊗[R] N))
                      (ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
                        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                          f))
                      x)
                    (x ⊗ₜ[R] (↑a : N)) ⋯,
                map_add' := ⋯, map_smul' := ⋯ :
                ↥f.ker →ₗ[R]
                  ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
                      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                          (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                        f)) }
              {
                toFun := fun (a : ↥f.ker) ↦
                  Subtype.mk (p := fun (x : M ⊗[R] N) ↦
                    Membership.mem (γ := Submodule S (M ⊗[R] N))
                      (ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
                        (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                            (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                          f))
                      x)
                    (y ⊗ₜ[R] (↑a : N)) ⋯,
                map_add' := ⋯, map_smul' := ⋯ :
                ↥f.ker →ₗ[R]
                  ↥(ker (R₂ := S) (M₂ := M ⊗[R] P) (τ₁₂ := RingHom.id S)
                      (((AlgebraTensorModule.lTensor S M : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[S] M ⊗[R] P) :
                          (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P)
                        f)) } :
            (a : ↥f.ker) → ↥((AlgebraTensorModule.lTensor S M : (a : N →ₗ[R] P) → M ⊗[R] N →ₗ[S] M ⊗[R] P) f).ker)
          x_1) :
      M ⊗[R] N)

Tactic:
simp [add_tmul]

Premises used: TensorProduct.add_tmul