-- 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
zero :
  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)
        0 :
      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) 0) :
      S ⊗[R] M)
tmul :
  ∀ (x y : S),
    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)
          (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) (1 ⊗ₜ[R] r) (x ⊗ₜ[R] y)) :
        S ⊗[R] M)
⊢ 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)
have add : ∀ (x y : S ⊗[R] S),
  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)
          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)
          (1 ⊗ₜ[R] r * x) :
        S ⊗[R] M) →
    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)
            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)
            (1 ⊗ₜ[R] r * y) :
          S ⊗[R] M) →
      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)
            (x + 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)
            (1 ⊗ₜ[R] r * (x + y)) :
          S ⊗[R] M)
Tactic: induction elem R S using TensorProduct.induction_on