-- 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 : 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
g : M →ₗ[R] Q
r : S
x : N
F : S →ₗ[R] M →ₗ[R] Q :=
  (↑R :
      {S M : Type v₃} →
        {M₂ : Type (max u_3 v₁)} →
          [inst : Semiring R] →
            [inst_15 : Semiring S] →
              [inst_16 : AddCommMonoid M] →
                [inst_17 : AddCommMonoid M₂] →
                  [inst_18 : Module R M] →
                    [inst_19 : Module R M₂] →
                      [inst_20 : Module S M] →
                        [inst_21 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := S)
    (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
        (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
      g)
hF :
  ∀ (s : S) (m : M),
    (IsTensorProduct.lift h F : (a : N) → Q) (HSMul.hSMul (β := N) s ((f : (a : M) → N) m : N)) =
      HSMul.hSMul (β := Q) s ((g : (a : M) → Q) m : Q)
change :
  (IsTensorProduct.lift h F : (a : N) → Q) (r • x) =
    HSMul.hSMul (β := Q) r ((IsTensorProduct.lift h F : (a : N) → Q) x : Q)
⊢ AddHom.toFun
      (LinearMap.toAddHom
        (IsTensorProduct.lift h
          ((↑R :
              {S M : Type v₃} →
                {M₂ : Type (max u_3 v₁)} →
                  [inst : Semiring R] →
                    [inst_15 : Semiring S] →
                      [inst_16 : AddCommMonoid M] →
                        [inst_17 : AddCommMonoid M₂] →
                          [inst_18 : Module R M] →
                            [inst_19 : Module R M₂] →
                              [inst_20 : Module S M] →
                                [inst_21 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := S)
            (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) : (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
                (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
              g))))
      (r • x) =
    HSMul.hSMul (α := S) (β := Q) ((RingHom.id S : (a : S) → S) r : S)
      (AddHom.toFun
        (LinearMap.toAddHom
          (IsTensorProduct.lift h
            ((↑R :
                {S M : Type v₃} →
                  {M₂ : Type (max u_3 v₁)} →
                    [inst : Semiring R] →
                      [inst_15 : Semiring S] →
                        [inst_16 : AddCommMonoid M] →
                          [inst_17 : AddCommMonoid M₂] →
                            [inst_18 : Module R M] →
                              [inst_19 : Module R M₂] →
                                [inst_20 : Module S M] →
                                  [inst_21 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (S := S)
              (((LinearMap.flip (Algebra.linearMap S (Module.End S (M →ₗ[R] Q))) :
                    (M →ₗ[R] Q) →ₗ[S] S →ₗ[S] M →ₗ[R] Q) :
                  (a : M →ₗ[R] Q) → S →ₗ[S] M →ₗ[R] Q)
                g))))
        x)

Tactic:
change h.lift F (r • x) = r • h.lift F x

Premises used: IsBaseChange.lift, HSMul.hSMul, DFunLike.coe