-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal S) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal S) → [inst : P.IsMaximal] → Module.{u_2, u_4} S (Mₚ P)
inst_10 : ∀ (P : Ideal S) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_2, u_4} R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id S) M (Mₚ P)
inst_11 : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime (M' := Mₚ P) P (f P)
H :
  ∀ (P : Ideal S) [inst_12 : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_13 : AddCommMonoid P_1] [inst_14 : Module R P_1]
    (N : Submodule R P_1),
    Function.Injective (α := TensorProduct.{u_1, u_4, u_1} R (Mₚ P) ↥N) (β :=
      TensorProduct.{u_1, u_4, u_1} R (Mₚ P) P_1) (⇑(lTensor (Mₚ P) N.subtype) : (a : Mₚ P ⊗[R] ↥N) → Mₚ P ⊗[R] P_1)
refine :
  ∀ (x : Type u_1) (x_1 : AddCommMonoid x) (x_2 : Module R x) (N : Submodule R x) (P : Ideal S) (hP : P.IsMaximal),
    Function.Injective (α := TensorProduct.{u_1, u_4, u_1} R (Mₚ P) ↥N) (β := TensorProduct.{u_1, u_4, u_1} R (Mₚ P) x)
      (⇑((IsLocalizedModule.map P.primeCompl
                  ((fun (P : Ideal S) [P.IsMaximal] ↦
                      (((AlgebraTensorModule.rTensor R ↥N :
                              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id S) M (Mₚ P) →ₗ[R]
                                M ⊗[R] ↥N →ₗ[S] TensorProduct.{u_1, u_4, u_1} R (Mₚ P) ↥N) :
                            (a : M →ₗ[S] Mₚ P) → M ⊗[R] ↥N →ₗ[S] Mₚ P ⊗[R] ↥N)
                          (f P) :
                        M ⊗[R] ↥N →ₗ[S] TensorProduct.{u_1, u_4, u_1} R (Mₚ P) ↥N))
                    P)
                  ((fun (P : Ideal S) [P.IsMaximal] ↦
                      (((AlgebraTensorModule.rTensor R x :
                              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id S) M (Mₚ P) →ₗ[R]
                                M ⊗[R] x →ₗ[S] TensorProduct.{u_1, u_4, u_1} R (Mₚ P) x) :
                            (a : M →ₗ[S] Mₚ P) → M ⊗[R] x →ₗ[S] Mₚ P ⊗[R] x)
                          (f P) :
                        M ⊗[R] x →ₗ[S] TensorProduct.{u_1, u_4, u_1} R (Mₚ P) x))
                    P) :
                (a : M ⊗[R] ↥N →ₗ[S] M ⊗[R] x) → Mₚ P ⊗[R] ↥N →ₗ[S] Mₚ P ⊗[R] x)
              (((AlgebraTensorModule.lTensor S M : (↥N →ₗ[R] x) →ₗ[R] M ⊗[R] ↥N →ₗ[S] M ⊗[R] x) :
                  (a : ↥N →ₗ[R] x) → M ⊗[R] ↥N →ₗ[S] M ⊗[R] x)
                N.subtype) :
            TensorProduct.{u_1, u_4, u_1} R (Mₚ P) ↥N →ₗ[S] TensorProduct.{u_1, u_4, u_1} R (Mₚ P) x) :
        (a : Mₚ P ⊗[R] ↥N) → Mₚ P ⊗[R] x)
⊢ ∀ ⦃P : Type u_1⦄ [inst_12 : AddCommMonoid P] [inst_13 : Module R P] (N : Submodule R P),
    Function.Injective (α := M ⊗[R] ↥N) (β := M ⊗[R] P)
      (⇑(((AlgebraTensorModule.lTensor S M : (↥N →ₗ[R] P) →ₗ[R] M ⊗[R] ↥N →ₗ[S] M ⊗[R] P) :
                (a : ↥N →ₗ[R] P) → M ⊗[R] ↥N →ₗ[S] M ⊗[R] P)
              N.subtype :
            M ⊗[R] ↥N →ₗ[S] M ⊗[R] P) :
        (a : M ⊗[R] ↥N) → M ⊗[R] P)

Tactic:
refine fun _ _ _ N ↦ injective_of_isLocalized_maximal _
    (fun P ↦ AlgebraTensorModule.rTensor R _ (f P)) _
    (fun P ↦ AlgebraTensorModule.rTensor R _ (f P)) _ fun P hP ↦ ?_

Premises used: TensorProduct.AlgebraTensorModule.rTensor, injective_of_isLocalized_maximal, TensorProduct, DFunLike.coe