-- 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)
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' := ⋯,
                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))
    (hy :
      (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 • 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' := ⋯, map_smul' := ⋯ : 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' := ⋯,
              map_smul' := ⋯ } :
          (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' := ⋯, map_smul' := ⋯ : S →ₗ[R] (M →ₗ[R] N) →ₗ[R] M →ₗ[R] P } :
              (a : S ⊗[R] (M →ₗ[R] N)) → M →ₗ[R] P)
            (x + y) :
          M →ₗ[R] P)
⊢ (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 tmul : ∀ (t : S) (f : M →ₗ[R] N),
  (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)
      (HSMul.hSMul (β := S ⊗[R] (M →ₗ[R] N)) s (t ⊗ₜ[R] f)) =
    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)
          (t ⊗ₜ[R] f) :
        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