-- 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)
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))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg :
  ∀ (x : M),
    Eq (α := ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
      ((g : (a : N) → ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) ((f : (a : M) → N) x) : ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
      (((↑(LinearEquiv.symm ULift.moduleEquiv) : S ⊗[R] M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) :
            (a : S ⊗[R] M) → ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
          (((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1 : (a : M) → S ⊗[R] M) x) :
        ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
refine_1 :
  (↑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₂)
        ((↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[S] ULift.{max v₁ v₃, v₂} N) ∘ₗ
          f'' ∘ₗ (↑ULift.moduleEquiv : ULift.{v₂, max v₁ v₃} (S ⊗[R] M) →ₗ[S] S ⊗[R] M) ∘ₗ g) ∘ₗ
      f =
    (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[R] ULift.{max v₁ v₃, v₂} N) ∘ₗ f
⊢ (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[S] ULift.{max v₁ v₃, v₂} N) ∘ₗ
      f'' ∘ₗ (↑ULift.moduleEquiv : ULift.{v₂, max v₁ v₃} (S ⊗[R] M) →ₗ[S] S ⊗[R] M) ∘ₗ g =
    (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[S] ULift.{max v₁ v₃, v₂} N) ∘ₗ LinearMap.id

Tactic:
refine (h (ULift.{max v₁ v₃} N) <| ULift.moduleEquiv.symm.toLinearMap.comp f).unique ?_ rfl