-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
    [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q),
    ∃! g' : N →ₗ[S] Q,
      (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type (max (max v₁ v₂) v₃)} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg :
  Eq (α := M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type (max (max v₁ v₂) v₃)} →
                [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₂)
        g ∘ₗ
      f)
    ((↑(LinearEquiv.symm ULift.moduleEquiv) : S ⊗[R] M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) ∘ₗ
      (mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)
f' : S ⊗[R] M →ₗ[R] N :=
  TensorProduct.lift
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ v₂)} →
            [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₂)
      (S := S)
      (((LinearMap.flip (AlgHom.toLinearMap (Algebra.ofId S (Module.End S (M →ₗ[R] N)))) :
            (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
        f))
s : S
x_1 x y : S ⊗[R] M
hx : (f' : (a : S ⊗[R] M) → N) (s • x) = HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) x : N)
hy : (f' : (a : S ⊗[R] M) → N) (s • y) = HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) y : N)
refine_2 : (f' : (a : S ⊗[R] M) → N) (s • x + s • y) = HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) (x + y) : N)
refine_2₁ :
  HAdd.hAdd (α := N) (β := N) ((f' : (a : S ⊗[R] M) → N) (s • x) : N) ((f' : (a : S ⊗[R] M) → N) (s • y) : N) =
    HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) (x + y) : N)
refine_2₂ :
  HAdd.hAdd (α := N) (β := N) ((f' : (a : S ⊗[R] M) → N) (s • x) : N) ((f' : (a : S ⊗[R] M) → N) (s • y) : N) =
    s • HAdd.hAdd (α := N) (β := N) ((f' : (a : S ⊗[R] M) → N) x : N) ((f' : (a : S ⊗[R] M) → N) y : N)
refine_2₃ :
  HAdd.hAdd (α := N) (β := N) ((f' : (a : S ⊗[R] M) → N) (s • x) : N) ((f' : (a : S ⊗[R] M) → N) (s • y) : N) =
    HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) x : N) + HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) y : N)
refine_2₄ :
  HAdd.hAdd (β := N) (HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) x : N))
      ((f' : (a : S ⊗[R] M) → N) (s • y) : N) =
    HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) x : N) + HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) y : N)
refine_2₅ refine_2₆ :
  HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) x : N) + HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) y : N) =
    HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) x : N) + HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) y : N)
⊢ (f' : (a : S ⊗[R] M) → N) (s • (x + y)) = HSMul.hSMul (β := N) s ((f' : (a : S ⊗[R] M) → N) (x + y) : N)

Tactic:
rw [smul_add, map_add, map_add, smul_add, hx, hy]

Premises used: map_add, smul_add