-- Mathlib/RingTheory/Flat/Localization.lean
theorem flat_of_isLocalized_maximal (H : ∀ (P : Ideal S) [P.IsMaximal], Flat R (Mₚ P)) :
    Module.Flat R M

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [inst : P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑((AlgebraTensorModule.lTensor S M) N.subtype)

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 ↦ ?_

Result:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [inst : P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
x✝² : Type u_1
x✝¹ : AddCommMonoid x✝²
x✝ : Module R x✝²
N : Submodule R x✝²
P : Ideal S
hP : P.IsMaximal
⊢ Function.Injective
    ⇑((IsLocalizedModule.map P.primeCompl ((fun P [P.IsMaximal] => (AlgebraTensorModule.rTensor R ↥N) (f P)) P)
          ((fun P [P.IsMaximal] => (AlgebraTensorModule.rTensor R x✝²) (f P)) P))
        ((AlgebraTensorModule.lTensor S M) N.subtype))

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [inst : P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
x✝² : Type u_1
x✝¹ : AddCommMonoid x✝²
x✝ : Module R x✝²
N : Submodule R x✝²
P : Ideal S
hP : P.IsMaximal
⊢ Function.Injective
    ⇑((IsLocalizedModule.map P.primeCompl ((fun P [P.IsMaximal] => (AlgebraTensorModule.rTensor R ↥N) (f P)) P)
          ((fun P [P.IsMaximal] => (AlgebraTensorModule.rTensor R x✝²) (f P)) P))
        ((AlgebraTensorModule.lTensor S M) N.subtype))

Tactic:
simpa [IsLocalizedModule.map_lTensor] using H P N

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [inst : P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal S) [inst : P.IsMaximal], Flat R (Mₚ P)
⊢ Flat R M

Tactic:
simp_rw [Flat.iff_lTensor_injectiveₛ] at H ⊢

Result:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [inst : P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(lTensor M N.subtype)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [inst : P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(lTensor M N.subtype)

Tactic:
simp_rw [← AlgebraTensorModule.coe_lTensor (A := S)]

Result:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [inst : P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑((AlgebraTensorModule.lTensor S M) N.subtype)