-- Module: Mathlib.RingTheory.Unramified.Finite
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
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
r : S
m : M
trans :
  Eq (α := S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                (r • m)) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (elem R S) :
      S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                m) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) :
      S ⊗[R] M)
trans₁ :
  ((TensorProduct.AlgebraTensorModule.map LinearMap.id
            (((LinearMap.flip
                    (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                  M →ₗ[R] S →ₗ[R] M) :
                (a : M) → S →ₗ[R] M)
              m) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) =
    HSMul.hSMul (β := S ⊗[R] M) r
      (((TensorProduct.AlgebraTensorModule.map LinearMap.id
                (((LinearMap.flip
                        (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                      M →ₗ[R] S →ₗ[R] M) :
                    (a : M) → S →ₗ[R] M)
                  m) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (elem R S) :
        S ⊗[R] M)
⊢ ((TensorProduct.AlgebraTensorModule.map LinearMap.id
            (((LinearMap.flip
                    (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                  M →ₗ[R] S →ₗ[R] M) :
                (a : M) → S →ₗ[R] M)
              (r • m)) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (elem R S) =
    HSMul.hSMul (β := S ⊗[R] M) r
      (((TensorProduct.AlgebraTensorModule.map LinearMap.id
                (((LinearMap.flip
                        (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                      M →ₗ[R] S →ₗ[R] M) :
                    (a : M) → S →ₗ[R] M)
                  m) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (elem R S) :
        S ⊗[R] M)

Tactic:
trans (TensorProduct.AlgebraTensorModule.map (LinearMap.id (R := S) (M := S))
      ((LinearMap.flip (AlgHom.toLinearMap (lsmul R R M))) m)) ((1 ⊗ₜ r) * elem R S)

Premises used: AlgHom.toLinearMap, LinearMap.id, HMul.hMul, Algebra.FormallyUnramified.elem, Algebra.lsmul, LinearMap.flip, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe, TensorProduct.AlgebraTensorModule.map