-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangeHom (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R N
P : Type u_5
inst_7 : AddCommMonoid P
inst_8 : Module R P
inst_9 : Module S P
inst_10 : IsScalarTower R S P
ε : N →ₗ[R] P
s : S
x : S ⊗[R] (M →ₗ[R] N)
zero :
  (TensorProduct.lift
          { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
      (HSMul.hSMul (β := S ⊗[R] (M →ₗ[R] N)) s 0) =
    HSMul.hSMul (β := M →ₗ[R] P) s
      ((TensorProduct.lift
            { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := ⋯,
              map_smul' := ⋯ : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
          (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
        0)
⊢ (TensorProduct.lift
          { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
      (s • x) =
    HSMul.hSMul (β := M →ₗ[R] P) s
      ((TensorProduct.lift
              { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := ⋯,
                map_smul' := ⋯ : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
            (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
          x :
        M →ₗ[R] P)
have add : ∀ (x y : S ⊗[R] (M →ₗ[R] N))
  (hx :
    (TensorProduct.lift
            { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := sorry,
              map_smul' := sorry } :
          (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
        (s • x) =
      HSMul.hSMul (β := M →ₗ[R] P) s
        ((TensorProduct.lift
                { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε),
                  map_add' := sorry, map_smul' := sorry : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
              (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
            x :
          M →ₗ[R] P))
  (hy :
    (TensorProduct.lift
            { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := sorry,
              map_smul' := sorry } :
          (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
        (s • y) =
      HSMul.hSMul (β := M →ₗ[R] P) s
        ((TensorProduct.lift
                { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε),
                  map_add' := sorry, map_smul' := sorry : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
              (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
            y :
          M →ₗ[R] P)),
  (TensorProduct.lift
          { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := sorry,
            map_smul' := sorry } :
        (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
      (s • (x + y)) =
    HSMul.hSMul (β := M →ₗ[R] P) s
      ((TensorProduct.lift
              { toFun := fun (s : S) ↦ HSMul.hSMul (β := (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P) s (compRight R ε), map_add' := sorry,
                map_smul' := sorry : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
            (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
          (x + y) :
        M →ₗ[R] P)
Tactic: induction x using TensorProduct.induction_on with
    | zero => simp
    | add x y hx hy => simp [smul_add, hx, hy]
    | tmul t f => simp [TensorProduct.smul_tmul', mul_smul]
Cleared hypotheses: x