-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M₁_1 : Type u_2
M₂_1 : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁_1
inst_2 : AddCommMonoid M₂_1
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M₁_1
inst_6 : Module R_1 M₂_1
inst_7 : Module R_1 M
inst_8 : Module R_1 M'
f_1 : M₁_1 →ₗ[R_1] M₂_1 →ₗ[R_1] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_9 : AddCommMonoid N₁
inst_10 : AddCommMonoid N₂
inst_11 : AddCommMonoid N
inst_12 : Module R_1 N₁
inst_13 : Module R_1 N₂
inst_14 : Module R_1 N
g_1 : N₁ →ₗ[R_1] N₂ →ₗ[R_1] N
R : Type u_9
S : Type u_10
inst_15 : CommSemiring R
inst_16 : CommSemiring S
inst_17 : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst_18 : AddCommMonoid M₁
inst_19 : AddCommMonoid M₂
inst_20 : AddCommMonoid M₃
inst_21 : AddCommMonoid M₁₂
inst_22 : AddCommMonoid M₂₃
inst_23 : Module R M₁
inst_24 : Module R M₂
inst_25 : Module S M₂
inst_26 : IsScalarTower R S M₂
inst_27 : Module R M₃
inst_28 : Module S M₃
inst_29 : IsScalarTower R S M₃
inst_30 : Module R M₁₂
inst_31 : Module S M₁₂
inst_32 : IsScalarTower R S M₁₂
inst_33 : Module R M₂₃
inst_34 : Module S M₂₃
inst_35 : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
this_1 : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), HSMul.hSMul (β := M₁ ⊗[R] M₂) s (y ⊗ₜ[R] x) = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x : M₂ ⊗[R] M₁
zero :
  AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂))
      (HSMul.hSMul (β := M₂ ⊗[R] M₁) s 0) =
    HSMul.hSMul (α := S) (β := M₁ ⊗[R] M₂) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) 0)
tmul :
  ∀ (x : M₂) (y : M₁),
    AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂))
        (HSMul.hSMul (β := M₂ ⊗[R] M₁) s (x ⊗ₜ[R] y)) =
      HSMul.hSMul (α := S) (β := M₁ ⊗[R] M₂) ((RingHom.id S : (a : S) → S) s : S)
        (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (x ⊗ₜ[R] y))
⊢ AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (s • x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
      (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) x)
have add : ∀ (x y : M₂ ⊗[R] M₁),
  AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (s • x) =
      HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
        (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) x) →
    AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (s • y) =
        HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
          (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) y) →
      AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (s • (x + y)) =
        HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) s : S)
          (AddHom.toFun (LinearMap.toAddHom (↑(TensorProduct.comm R M₂ M₁) : M₂ ⊗[R] M₁ →ₗ[R] M₁ ⊗[R] M₂)) (x + y))
Tactic: induction x
Cleared hypotheses: x