-- 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
x : M
induction :
  ∀ (x_1 : S ⊗[R] S),
    (_root_.TensorProduct.lift
            ((↑R :
                {S M : Type u_2} →
                  {M₂ : Type u_3} →
                    [inst : Semiring R] →
                      [inst_9 : Semiring S] →
                        [inst_10 : AddCommMonoid M] →
                          [inst_11 : AddCommMonoid M₂] →
                            [inst_12 : Module R M] →
                              [inst_13 : Module R M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (LinearMap.flip
                  ((↑R :
                      {S : Type u_2} →
                        {M : Type u_3} →
                          {M₂ : Type (max u_3 u_2)} →
                            [inst : Semiring R] →
                              [inst_9 : Semiring S] →
                                [inst_10 : AddCommMonoid M] →
                                  [inst_11 : AddCommMonoid M₂] →
                                    [inst_12 : Module R M] →
                                      [inst_13 : Module R M₂] →
                                        [inst_14 : Module S M] →
                                          [inst_15 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (LinearMap.flip
                        (AlgHom.toLinearMap (lsmul S S M) : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) S (End S M)) :
                      M →ₗ[S] S →ₗ[S] M)) :
                LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) S (M →ₗ[R] M))) :
          (a : S ⊗[R] M) → 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)
                    x) :
                S ⊗[R] S →ₗ[S] S ⊗[R] M) :
              (a : S ⊗[R] S) → S ⊗[R] M)
            x_1 :
          S ⊗[R] M) =
      HSMul.hSMul (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) x_1 : S) x
⊢ (_root_.TensorProduct.lift
          ((↑R :
              {S M : Type u_2} →
                {M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (LinearMap.flip
                ((↑R :
                    {S : Type u_2} →
                      {M : Type u_3} →
                        {M₂ : Type (max u_3 u_2)} →
                          [inst : Semiring R] →
                            [inst_9 : Semiring S] →
                              [inst_10 : AddCommMonoid M] →
                                [inst_11 : AddCommMonoid M₂] →
                                  [inst_12 : Module R M] →
                                    [inst_13 : Module R M₂] →
                                      [inst_14 : Module S M] →
                                        [inst_15 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (LinearMap.flip
                      (AlgHom.toLinearMap (lsmul S S M) : LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) S (End S M)) :
                    M →ₗ[S] S →ₗ[S] M)) :
              LinearMap.{u_2, u_2, u_2, u_3} (RingHom.id S) S (M →ₗ[R] M))) :
        (a : S ⊗[R] M) → 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)
                  x) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (elem R S) :
        S ⊗[R] M) =
    HSMul.hSMul (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) (elem R S) : S) x

Tactic:
induction elem R S using TensorProduct.induction_on with
    | zero => simp
    | tmul r s => simp [mul_smul, smul_comm r s]
    | add y z hy hz => simp [hy, hz, add_smul]

Premises used: Algebra.FormallyUnramified.elem, add_smul, SemigroupAction.mul_smul