-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
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
this : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S) = HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)
zero :
  ((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) (r ⊗ₜ[R] 1) 0) =
    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)
        0)
tmul :
  ∀ (x y : S),
    ((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) (r ⊗ₜ[R] 1) (x ⊗ₜ[R] y)) =
      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)
            (x ⊗ₜ[R] y) :
          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) (r ⊗ₜ[R] 1) (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)
have add : ∀ (x y : S ⊗[R] S),
  ((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)
        (r ⊗ₜ[R] 1 * x) =
      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)
            x :
          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)
          (r ⊗ₜ[R] 1 * y) =
        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)
              y :
            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)
          (r ⊗ₜ[R] 1 * (x + y)) =
        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)
              (x + y) :
            S ⊗[R] M)
Tactic: induction elem R S using TensorProduct.induction_on