awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
simp :
  ((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)
⊢ AddHom.toFun
      (LinearMap.toAddHom
        ((((LinearMap.flip
                    (((TensorProduct.AlgebraTensorModule.mapBilinear R S S S S S M :
                          (S →ₗ[S] S) →ₗ[S] (S →ₗ[R] M) →ₗ[R] S ⊗[R] S →ₗ[S] S ⊗[R] M) :
                        (a : S →ₗ[S] S) → (S →ₗ[R] M) →ₗ[R] S ⊗[R] S →ₗ[S] S ⊗[R] M)
                      LinearMap.id) :
                  S ⊗[R] S →ₗ[S] (S →ₗ[R] M) →ₗ[R] S ⊗[R] M) :
                (a : S ⊗[R] S) → (S →ₗ[R] M) →ₗ[R] S ⊗[R] M)
              (elem R S) :
            (S →ₗ[R] M) →ₗ[R] S ⊗[R] M) ∘ₗ
          (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)))
      (r • m) =
    HSMul.hSMul (α := S) (β := S ⊗[R] M) ((RingHom.id S : (a : S) → S) r : S)
      (AddHom.toFun
        (LinearMap.toAddHom
          ((((LinearMap.flip
                      (((TensorProduct.AlgebraTensorModule.mapBilinear R S S S S S M :
                            (S →ₗ[S] S) →ₗ[S] (S →ₗ[R] M) →ₗ[R] S ⊗[R] S →ₗ[S] S ⊗[R] M) :
                          (a : S →ₗ[S] S) → (S →ₗ[R] M) →ₗ[R] S ⊗[R] S →ₗ[S] S ⊗[R] M)
                        LinearMap.id) :
                    S ⊗[R] S →ₗ[S] (S →ₗ[R] M) →ₗ[R] S ⊗[R] M) :
                  (a : S ⊗[R] S) → (S →ₗ[R] M) →ₗ[R] S ⊗[R] M)
                (elem R S) :
              (S →ₗ[R] M) →ₗ[R] S ⊗[R] M) ∘ₗ
            (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)))
        m)

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.flip_apply, TensorProduct.AlgebraTensorModule.mapBilinear_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, AddHom.toFun_eq_coe, LinearMap.flip_apply, TensorProduct.AlgebraTensorModule.mapBilinear_apply, LinearMap.coe_comp, LinearMap.coe_toAddHom, Function.comp_apply
-- 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
⊢ 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)

Tactic:
simp
-- 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
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)

Tactic:
simp [smul_comm r]

Premises used: SMulCommClass.smul_comm
-- 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
x y : S ⊗[R] S
h :
  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)
h_1 :
  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:
simp only [map_add, mul_add, *]

Premises used: map_add, mul_add
-- 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
⊢ HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (r ⊗ₜ[R] 1) * elem R S = 0

Tactic:
have := one_tmul_sub_tmul_one_mul_elem (R := R) r
-- 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
this : HSub.hSub (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (r ⊗ₜ[R] 1) * elem R S = 0
⊢ HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S) = HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)

Tactic:
rw [sub_mul, sub_eq_zero] at this

Premises used: sub_eq_zero, sub_mul
-- 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
this : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S) = HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)
rw :
  ((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)
⊢ ((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)

Tactic:
rw [this]
-- 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
this : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S) = HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem 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)
      (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)

Tactic:
simp
-- 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
this : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S) = HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)
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:
simp [TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- 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
this : HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S) = HMul.hMul (α := S ⊗[R] S) (r ⊗ₜ[R] 1) (elem R S)
x y : S ⊗[R] S
h :
  ((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)
h_1 :
  ((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:
simp only [map_add, smul_add, mul_add, *]

Premises used: map_add, mul_add, smul_add
-- 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
h :
  ∀ (x : M),
    Eq (α := M)
      (((TensorProduct.AlgebraTensorModule.lift
                  (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))) :
                S ⊗[R] M →ₗ[S] M) ∘ₗ
              (sec R S M : M →ₗ[S] S ⊗[R] M) :
            (a : M) → M)
          x :
        M)
      ((LinearMap.id : (a : M) → M) x : M)
⊢ Eq (α := M →ₗ[S] M)
    ((TensorProduct.AlgebraTensorModule.lift
          (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))) :
        S ⊗[R] M →ₗ[S] M) ∘ₗ
      (sec R S M : M →ₗ[S] S ⊗[R] M))
    LinearMap.id

Tactic:
ext x
-- 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
⊢ (_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)
        0) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((TensorProduct.lmul' R : (a : S ⊗[R] S) → S) 0 : S) x

Tactic:
simp