-- Module: Mathlib.RingTheory.Flat.Domain
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : Type u_4
Q : Type u_5
inst_6 : AddCommGroup P
inst_7 : Module R P
inst_8 : AddCommGroup Q
inst_9 : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst_10 : Module.Flat R Q
hf : Injective.{u_4 + 1, u_2 + 1} (α := P) (β := M) (⇑f : (a : P) → M)
hg : Injective.{u_5 + 1, u_3 + 1} (α := Q) (β := N) (⇑g : (a : Q) → N)
K : Type u_1 := FractionRing R
H₁ :
  Injective (α := K ⊗[R] P ⊗[K] (K ⊗[R] Q)) (β := K ⊗[R] M ⊗[K] (K ⊗[R] N))
    (⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) :
      (a : K ⊗[R] P ⊗[K] (K ⊗[R] Q)) → K ⊗[R] M ⊗[K] (K ⊗[R] N))
H₂ :
  Injective (α := K ⊗[R] P ⊗[R] Q) (β := K ⊗[R] P ⊗[K] (K ⊗[R] Q))
    (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q) :
          K ⊗[R] P ⊗[R] Q ≃ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
      (a : K ⊗[R] P ⊗[R] Q) → K ⊗[R] P ⊗[K] (K ⊗[R] Q))
H₃ :
  Injective (α := K ⊗[R] M ⊗[K] (K ⊗[R] N)) (β := K ⊗[R] M ⊗[R] N)
    (⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N : K ⊗[R] M ⊗[K] (K ⊗[R] N) ≃ₗ[K] K ⊗[R] M ⊗[R] N) :
      (a : K ⊗[R] M ⊗[K] (K ⊗[R] N)) → K ⊗[R] M ⊗[R] N)
H₄ :
  Injective (α := K ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] P ⊗[R] Q)
    (⇑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q) : K ⊗[R] (P ⊗[R] Q) ≃ₗ[K] K ⊗[R] P ⊗[R] Q) :
      (a : K ⊗[R] (P ⊗[R] Q)) → K ⊗[R] P ⊗[R] Q)
H₅ :
  Injective (α := K ⊗[R] M ⊗[R] N) (β := K ⊗[R] (M ⊗[R] N))
    (⇑(AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
      (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
H₆ :
  Injective (α := R ⊗[R] (P ⊗[R] Q)) (β := K ⊗[R] (P ⊗[R] Q))
    (⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K)) : (a : R ⊗[R] (P ⊗[R] Q)) → K ⊗[R] (P ⊗[R] Q))
H₇ :
  Injective (α := P ⊗[R] Q) (β := R ⊗[R] (P ⊗[R] Q))
    (⇑(LinearEquiv.symm (TensorProduct.lid R (P ⊗[R] Q))) : (a : P ⊗[R] Q) → R ⊗[R] (P ⊗[R] Q))
p : P
q : Q
h :
  Eq (α := K ⊗[R] (M ⊗[R] N)) (1 ⊗ₜ[R] ((f : (a : P) → M) p ⊗ₜ[R] (g : (a : Q) → N) q) : K ⊗[R] (M ⊗[R] N))
    (((AlgebraTensorModule.assoc R R K K M N : K ⊗[R] M ⊗[R] N ≃ₗ[K] K ⊗[R] (M ⊗[R] N)) :
          (a : K ⊗[R] M ⊗[R] N) → K ⊗[R] (M ⊗[R] N))
        (HSMul.hSMul (α := K) (β := K ⊗[R] M) 1
            ((algebraMap R K : (a : R) → K) 1 ⊗ₜ[R] (f : (a : P) → M) p : K ⊗[R] M) ⊗ₜ[R]
          (g : (a : Q) → N) q) :
      K ⊗[R] (M ⊗[R] N))
⊢ Eq (α := K ⊗[R] (M ⊗[R] N))
    (((((AlgebraTensorModule.curry ((mk R K (M ⊗[R] N) : (a : K) → M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) 1 ∘ₗ map f g) :
                  P →ₗ[R] Q →ₗ[R] K ⊗[R] (M ⊗[R] N)) :
                (a : P) → Q →ₗ[R] K ⊗[R] (M ⊗[R] N))
              p :
            Q →ₗ[R] K ⊗[R] (M ⊗[R] N)) :
          (a : Q) → K ⊗[R] (M ⊗[R] N))
        q :
      K ⊗[R] (M ⊗[R] N))
    (((((AlgebraTensorModule.curry
                    (((↑R :
                            {S : Type u_1} →
                              {M M₂ : Type (max (max u_1 u_2) u_3)} →
                                [inst : Semiring R] →
                                  [inst_11 : Semiring S] →
                                    [inst_12 : AddCommMonoid M] →
                                      [inst_13 : AddCommMonoid M₂] →
                                        [inst_14 : Module R M] →
                                          [inst_15 : Module R M₂] →
                                            [inst_16 : Module S M] →
                                              [inst_17 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                          ((↑(AlgebraTensorModule.assoc R R K K M N) : K ⊗[R] M ⊗[R] N →ₗ[K] K ⊗[R] (M ⊗[R] N)) :
                            K ⊗[R] M ⊗[R] N →ₗ[K] K ⊗[R] (M ⊗[R] N)) :
                        K ⊗[R] M ⊗[R] N →ₗ[R] K ⊗[R] (M ⊗[R] N)) ∘ₗ
                      ((↑R :
                              {S : Type u_1} →
                                {M M₂ : Type (max (max u_1 u_2) u_3)} →
                                  [inst : Semiring R] →
                                    [inst_11 : Semiring S] →
                                      [inst_12 : AddCommMonoid M] →
                                        [inst_13 : AddCommMonoid M₂] →
                                          [inst_14 : Module R M] →
                                            [inst_15 : Module R M₂] →
                                              [inst_16 : Module S M] →
                                                [inst_17 : Module S M₂] →
                                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                            ((↑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N) :
                                K ⊗[R] M ⊗[K] (K ⊗[R] N) →ₗ[K] K ⊗[R] M ⊗[R] N) :
                              K ⊗[R] M ⊗[K] (K ⊗[R] N) →ₗ[K] K ⊗[R] M ⊗[R] N) ∘ₗ
                          (↑R :
                                {S : Type u_1} →
                                  {M : Type (max (max u_1 u_4) u_5)} →
                                    {M₂ : Type (max (max u_1 u_2) u_3)} →
                                      [inst : Semiring R] →
                                        [inst_11 : Semiring S] →
                                          [inst_12 : AddCommMonoid M] →
                                            [inst_13 : AddCommMonoid M₂] →
                                              [inst_14 : Module R M] →
                                                [inst_15 : Module R M₂] →
                                                  [inst_16 : Module S M] →
                                                    [inst_17 : Module S M₂] →
                                                      [LinearMap.CompatibleSMul M M₂ R S] →
                                                        (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                              (map (LinearMap.baseChange K f) (LinearMap.baseChange K g)) ∘ₗ
                            ((↑R :
                                    {S : Type u_1} →
                                      {M M₂ : Type (max (max u_1 u_4) u_5)} →
                                        [inst : Semiring R] →
                                          [inst_11 : Semiring S] →
                                            [inst_12 : AddCommMonoid M] →
                                              [inst_13 : AddCommMonoid M₂] →
                                                [inst_14 : Module R M] →
                                                  [inst_15 : Module R M₂] →
                                                    [inst_16 : Module S M] →
                                                      [inst_17 : Module S M₂] →
                                                        [LinearMap.CompatibleSMul M M₂ R S] →
                                                          (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                                  ((↑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q)) :
                                      K ⊗[R] P ⊗[R] Q →ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
                                    K ⊗[R] P ⊗[R] Q →ₗ[K] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) :
                                K ⊗[R] P ⊗[R] Q →ₗ[R] K ⊗[R] P ⊗[K] (K ⊗[R] Q)) ∘ₗ
                              (((↑R :
                                        {S : Type u_1} →
                                          {M M₂ : Type (max (max u_1 u_4) u_5)} →
                                            [inst : Semiring R] →
                                              [inst_11 : Semiring S] →
                                                [inst_12 : AddCommMonoid M] →
                                                  [inst_13 : AddCommMonoid M₂] →
                                                    [inst_14 : Module R M] →
                                                      [inst_15 : Module R M₂] →
                                                        [inst_16 : Module S M] →
                                                          [inst_17 : Module S M₂] →
                                                            [LinearMap.CompatibleSMul M M₂ R S] →
                                                              (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                                      ((↑(LinearEquiv.symm (AlgebraTensorModule.assoc R R K K P Q)) :
                                          K ⊗[R] (P ⊗[R] Q) →ₗ[K] K ⊗[R] P ⊗[R] Q) :
                                        K ⊗[R] (P ⊗[R] Q) →ₗ[K] K ⊗[R] P ⊗[R] Q) :
                                    K ⊗[R] (P ⊗[R] Q) →ₗ[R] K ⊗[R] P ⊗[R] Q) ∘ₗ
                                  (LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K) ∘ₗ
                                      (↑(LinearEquiv.symm (TensorProduct.lid R (P ⊗[R] Q))) :
                                        P ⊗[R] Q →ₗ[R] R ⊗[R] (P ⊗[R] Q)) :
                                    P ⊗[R] Q →ₗ[R] K ⊗[R] (P ⊗[R] Q)) :
                                P ⊗[R] Q →ₗ[R] K ⊗[R] P ⊗[R] Q) :
                        P ⊗[R] Q →ₗ[R] K ⊗[R] M ⊗[R] N)) :
                  P →ₗ[R] Q →ₗ[R] K ⊗[R] (M ⊗[R] N)) :
                (a : P) → Q →ₗ[R] K ⊗[R] (M ⊗[R] N))
              p :
            Q →ₗ[R] K ⊗[R] (M ⊗[R] N)) :
          (a : Q) → K ⊗[R] (M ⊗[R] N))
        q :
      K ⊗[R] (M ⊗[R] N))

Tactic:
change (1 : K) ⊗ₜ[R] (f p ⊗ₜ[R] g q) = (AlgebraTensorModule.assoc R R K K M N)
    (((1 : K) • (algebraMap R K) 1 ⊗ₜ[R] f p) ⊗ₜ[R] g q)

Premises used: Algebra.algebraMap, HSMul.hSMul, TensorProduct.tmul, OfNat.ofNat, DFunLike.coe, TensorProduct.AlgebraTensorModule.assoc