-- 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)
⊢ ((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 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)
Tactic: induction elem R S using TensorProduct.induction_on