-- 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
s : Set S
spn : Eq (α := Ideal S) (Ideal.span s) ⊤
Mₛ : (↑s : Type u_2) → Type u_5
inst_7 : (r : (↑s : Type u_2)) → AddCommMonoid (Mₛ r)
inst_8 : (r : (↑s : Type u_2)) → Module.{u_1, u_5} R (Mₛ r)
inst_9 : (r : (↑s : Type u_2)) → Module.{u_2, u_5} S (Mₛ r)
inst_10 : ∀ (r : (↑s : Type u_2)), IsScalarTower.{u_1, u_2, u_5} R S (Mₛ r)
g : (r : (↑s : Type u_2)) → LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id S) M (Mₛ r)
inst_11 : ∀ (r : (↑s : Type u_2)), IsLocalizedModule.Away (↑r : S) (g r)
H :
  ∀ (r : (↑s : Type u_2)) ⦃P : Type u_1⦄ [inst_12 : AddCommMonoid P] [inst_13 : Module R P] (N : Submodule R P),
    Function.Injective (α := TensorProduct.{u_1, u_5, u_1} R (Mₛ r) ↥N) (β := TensorProduct.{u_1, u_5, u_1} R (Mₛ r) P)
      (⇑(lTensor (Mₛ r) N.subtype) : (a : Mₛ r ⊗[R] ↥N) → Mₛ r ⊗[R] P)
refine :
  ∀ (x : Type u_1) (x_1 : AddCommMonoid x) (x_2 : Module R x) (N : Submodule R x) (r : (↑s : Type u_2)),
    Function.Injective (α := TensorProduct.{u_1, u_5, u_1} R (Mₛ r) ↥N) (β := TensorProduct.{u_1, u_5, u_1} R (Mₛ r) x)
      (⇑((IsLocalizedModule.map (Submonoid.powers (↑r : S))
                  ((fun (r : (↑s : Type u_2)) ↦
                      (((AlgebraTensorModule.rTensor R ↥N :
                              LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id S) M (Mₛ r) →ₗ[R]
                                M ⊗[R] ↥N →ₗ[S] TensorProduct.{u_1, u_5, u_1} R (Mₛ r) ↥N) :
                            (a : M →ₗ[S] Mₛ r) → M ⊗[R] ↥N →ₗ[S] Mₛ r ⊗[R] ↥N)
                          (g r) :
                        M ⊗[R] ↥N →ₗ[S] TensorProduct.{u_1, u_5, u_1} R (Mₛ r) ↥N))
                    r)
                  ((fun (r : (↑s : Type u_2)) ↦
                      (((AlgebraTensorModule.rTensor R x :
                              LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id S) M (Mₛ r) →ₗ[R]
                                M ⊗[R] x →ₗ[S] TensorProduct.{u_1, u_5, u_1} R (Mₛ r) x) :
                            (a : M →ₗ[S] Mₛ r) → M ⊗[R] x →ₗ[S] Mₛ r ⊗[R] x)
                          (g r) :
                        M ⊗[R] x →ₗ[S] TensorProduct.{u_1, u_5, u_1} R (Mₛ r) x))
                    r) :
                (a : M ⊗[R] ↥N →ₗ[S] M ⊗[R] x) → Mₛ r ⊗[R] ↥N →ₗ[S] Mₛ r ⊗[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_5, u_1} R (Mₛ r) ↥N →ₗ[S] TensorProduct.{u_1, u_5, u_1} R (Mₛ r) x) :
        (a : Mₛ r ⊗[R] ↥N) → Mₛ r ⊗[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_span s spn _
    (fun r ↦ AlgebraTensorModule.rTensor R _ (g r)) _
    (fun r ↦ AlgebraTensorModule.rTensor R _ (g r)) _ fun r ↦ ?_

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