-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M_1 : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M_1
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M_1
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M_1 →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst_9 : AddCommMonoid P
inst_10 : Module R P
inst_11 : AddCommMonoid Q
inst_12 : Module S Q
inst_13 : Module R Q
inst_14 : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst_15 : CommSemiring T
inst_16 : Algebra R T
inst_17 : Algebra S T
inst_18 : IsScalarTower R S T
inst_19 : AddCommMonoid O
inst_20 : Module R O
inst_21 : Module S O
inst_22 : Module T O
inst_23 : IsScalarTower S T O
inst_24 : IsScalarTower R S O
inst_25 : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst_26 : CommSemiring R'
inst_27 : CommSemiring S'
inst_28 : Algebra R R'
inst_29 : Algebra S S'
inst_30 : Algebra R' S'
inst_31 : Algebra R S'
inst_32 : IsScalarTower R R' S'
inst_33 : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst_34 : CommRing A
inst_35 : CommRing B
inst_36 : Algebra R A
inst_37 : Algebra R B
inst_38 : Algebra A B
inst_39 : Algebra S B
inst_40 : IsScalarTower R A B
inst_41 : IsScalarTower R S B
inst_42 : IsPushout R S A B
M : Type u_10
inst_43 : AddCommGroup M
inst_44 : Module R M
inst_45 : Module A M
inst_46 : IsScalarTower R A M
s : S
x : S ⊗[R] M
zero :
  ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
        (a : S ⊗[R] M) → B ⊗[A] M)
      (HSMul.hSMul (β := S ⊗[R] M) s 0) =
    HSMul.hSMul (β := B ⊗[A] M) s
      (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
          (a : S ⊗[R] M) → B ⊗[A] M)
        0)
⊢ ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
        (a : S ⊗[R] M) → B ⊗[A] M)
      (s • x) =
    HSMul.hSMul (β := B ⊗[A] M) s
      (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
            (a : S ⊗[R] M) → B ⊗[A] M)
          x :
        B ⊗[A] M)
have add : ∀ (x y : S ⊗[R] M)
  (hx :
    ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
          (a : S ⊗[R] M) → B ⊗[A] M)
        (s • x) =
      HSMul.hSMul (β := B ⊗[A] M) s
        (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
              (a : S ⊗[R] M) → B ⊗[A] M)
            x :
          B ⊗[A] M))
  (hy :
    ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
          (a : S ⊗[R] M) → B ⊗[A] M)
        (s • y) =
      HSMul.hSMul (β := B ⊗[A] M) s
        (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
              (a : S ⊗[R] M) → B ⊗[A] M)
            y :
          B ⊗[A] M)),
  ((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
        (a : S ⊗[R] M) → B ⊗[A] M)
      (s • (x + y)) =
    HSMul.hSMul (β := B ⊗[A] M) s
      (((↑(LinearEquiv.symm (cancelBaseChangeAux R S A B M) : S ⊗[R] M ≃ₗ[R] B ⊗[A] M) : S ⊗[R] M ≃+ B ⊗[A] M) :
            (a : S ⊗[R] M) → B ⊗[A] M)
          (x + y) :
        B ⊗[A] M)
Tactic: induction x with
    | zero => simp
    | add x y hx hy => simp only [smul_add, map_add, hx, hy]
    | tmul s' m => simp [Algebra.smul_def, TensorProduct.smul_tmul']
Cleared hypotheses: x