-- 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))
h :
  ∀ (p : P) (q : Q),
    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))
⊢ Eq (α := P ⊗[R] Q →ₗ[R] K ⊗[R] (M ⊗[R] N))
    ((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))
    (((↑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))

Tactic:
ext p q