-- 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
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
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ (↑eM : M →ₗ[R] P) = (↑(LinearEquiv.restrictScalars R eN) : N →ₗ[R] Q) ∘ₗ f
this :
  ∀ (m : M),
    Eq.{u_3 + 1} (α := Q) ((f' : (a : P) → Q) ((eM : (a : M) → P) m : P) : Q)
      ((eN : (a : N) → Q) ((f : (a : M) → N) m : N) : Q)
refine_1 :
  ∀
    (ist :
      IsTensorProduct.{u_1, v₃, v₁, v₂} (M₁ := S) (M₂ := M) (M := N)
        ((↑R :
            {S M : Type v₃} →
              {M₂ : Type (max v₁ 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] N))) : (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
              (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
            f))),
    IsTensorProduct.{u_1, v₃, u_2, u_3} (M₁ := S) (M₂ := P) (M := Q)
      ((↑R :
          {S M : Type v₃} →
            {M₂ : Type (max u_2 u_3)} →
              [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 (P →ₗ[R] Q))) : (P →ₗ[R] Q) →ₗ[S] S →ₗ[S] P →ₗ[R] Q) :
            (a : P →ₗ[R] Q) → S →ₗ[S] P →ₗ[R] Q)
          f'))
refine_2 :
  ∀
    (ist :
      IsTensorProduct.{u_1, v₃, u_2, u_3} (M₁ := S) (M₂ := P) (M := Q)
        ((↑R :
            {S M : Type v₃} →
              {M₂ : Type (max u_2 u_3)} →
                [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 (P →ₗ[R] Q))) : (P →ₗ[R] Q) →ₗ[S] S →ₗ[S] P →ₗ[R] Q) :
              (a : P →ₗ[R] Q) → S →ₗ[S] P →ₗ[R] Q)
            f'))),
    IsTensorProduct.{u_1, v₃, v₁, v₂} (M₁ := S) (M₂ := M) (M := N)
      ((↑R :
          {S M : Type v₃} →
            {M₂ : Type (max v₁ 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] N))) : (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
            (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
          f))
⊢ IsTensorProduct.{u_1, v₃, v₁, v₂} (M₁ := S) (M₂ := M) (M := N)
      ((↑R :
          {S M : Type v₃} →
            {M₂ : Type (max v₁ 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] N))) : (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
            (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
          f)) ↔
    IsTensorProduct.{u_1, v₃, u_2, u_3} (M₁ := S) (M₂ := P) (M := Q)
      ((↑R :
          {S M : Type v₃} →
            {M₂ : Type (max u_2 u_3)} →
              [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 (P →ₗ[R] Q))) : (P →ₗ[R] Q) →ₗ[S] S →ₗ[S] P →ₗ[R] Q) :
            (a : P →ₗ[R] Q) → S →ₗ[S] P →ₗ[R] Q)
          f'))

Tactic:
refine ⟨fun ist ↦ ?_, fun ist ↦ ?_⟩