awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : Submonoid R
inst_3 : IsLocalization p S
P : Type u_1
x : AddCommMonoid P
x_1 : Module R P
N : Submodule R P
h :
  IsBaseChange (N :=
    ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)) S
    (Submodule.toLocalized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R]
  ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
x_2 : S
x_3 : ↥N
⊢ Eq (α := S ⊗[R] P)
    (((((AlgebraTensorModule.curry (lTensor S N.subtype) : S →ₗ[R] ↥N →ₗ[R] S ⊗[R] P) : (a : S) → ↥N →ₗ[R] S ⊗[R] P)
              x_2 :
            ↥N →ₗ[R] S ⊗[R] P) :
          (a : ↥N) → S ⊗[R] P)
        x_3 :
      S ⊗[R] P)
    ((↑((h.equiv :
              (a : S ⊗[R] ↥N.subtype.range) →
                ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range))
            (((↑(LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯)) :
                  S ⊗[R] ↥N →ₗ[R] S ⊗[R] ↥N.subtype.range) :
                (a : S ⊗[R] ↥N) → S ⊗[R] ↥N.subtype.range)
              ((((TensorProduct.mk R S ↥N : (a : S) → ↥N →ₗ[R] S ⊗[R] ↥N) x_2 : ↥N →ₗ[R] S ⊗[R] ↥N) :
                  (a : ↥N) → S ⊗[R] ↥N)
                x_3))) :
        S ⊗[R] P) :
      S ⊗[R] P)

Tactic:
simp [h.equiv_tmul, TensorProduct.smul_tmul']

Premises used: TensorProduct.smul_tmul', IsBaseChange.equiv_tmul
-- 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
p : Submonoid R
inst_3 : IsLocalization p S
P : Type u_1
x : AddCommMonoid P
x_1 : Module R P
N : Submodule R P
h :
  IsBaseChange (N :=
    ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)) S
    (Submodule.toLocalized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R]
  ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
⊢ lTensor S N.subtype =
    Submodule.subtype
        (Submodule.localized₀ p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range) ∘ₗ
      (↑e :
        S ⊗[R] ↥N →ₗ[R]
          ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range))

Tactic:
have : N.subtype.lTensor S = Submodule.subtype _ ∘ₗ e.toLinearMap := by
    ext; change _ = (h.equiv _).1; simp [h.equiv_tmul, TensorProduct.smul_tmul']
-- 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
p : Submonoid R
inst_3 : IsLocalization p S
P : Type u_1
x : AddCommMonoid P
x_1 : Module R P
N : Submodule R P
h :
  IsBaseChange (N :=
    ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)) S
    (Submodule.toLocalized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R]
  ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
this :
  lTensor S N.subtype =
    Submodule.subtype
        (Submodule.localized₀ p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range) ∘ₗ
      (↑e :
        S ⊗[R] ↥N →ₗ[R]
          ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range))
⊢ Function.Injective (α := S ⊗[R] ↥N) (β := S ⊗[R] P) (⇑(lTensor S N.subtype) : (a : S ⊗[R] ↥N) → S ⊗[R] P)

Tactic:
simpa [this] using e.injective

Premises used: LinearEquiv.injective
-- 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
p_1 : Submonoid R
inst_3 : IsLocalization p_1 S
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module.Flat R S
p : Submonoid S
⊢ Module.Flat.{u_1, u_2} R (Localization (M := S) p)

Tactic:
have : Module.Flat S (Localization p) := IsLocalization.flat _ p
  .trans R S _

Premises used: Localization, Module.Flat.trans, IsLocalization.flat
-- 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
p : Submonoid R
inst_3 : IsLocalization p S
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
⊢ Flat S M ↔ Flat R M

Tactic:
have := isLocalizedModule_id p M S
  have := IsLocalization.flat S p
  ⟨fun _ ↦ .trans R S M, fun _ ↦ .of_isLocalizedModule S p .id⟩

Premises used: LinearMap.id, isLocalizedModule_id, Module.Flat.trans, Iff.intro, IsLocalization.flat, Module.Flat.of_isLocalizedModule
-- 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], Flat.{u_1, u_4} R (Mₚ P)
simp_rw :
  ∀
    (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))
    ⦃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) (⇑(lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)
⊢ Flat R M

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

Premises used: Module.Flat.iff_lTensor_injectiveₛ
-- 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)
simp_rw :
  ∀ ⦃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)
⊢ ∀ ⦃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) (⇑(lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)

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

Premises used: TensorProduct.AlgebraTensorModule.coe_lTensor
-- 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)
⊢ ∀ ⦃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:
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, Membership.mem, Subtype, Submodule.subtype, TensorProduct, DFunLike.coe, TensorProduct.AlgebraTensorModule.lTensor
-- 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)
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)

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

Premises used: IsLocalizedModule.map_lTensor
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : ∀ (P : Ideal R) [inst_3 : P.IsMaximal], Flat R (LocalizedModule P.primeCompl M)
⊢ Flat R M

Tactic:
flat_of_isLocalized_maximal _ _ _ (fun _ _ ↦ mkLinearMap _ _) h

Premises used: Module.flat_of_isLocalized_maximal, LocalizedModule.mkLinearMap
-- 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)), Flat.{u_1, u_5} R (Mₛ r)
simp_rw :
  ∀
    (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))
    ⦃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) (⇑(lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)
⊢ Flat R M

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

Premises used: Module.Flat.iff_lTensor_injectiveₛ
-- 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)
simp_rw :
  ∀ ⦃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)
⊢ ∀ ⦃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) (⇑(lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)

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

Premises used: TensorProduct.AlgebraTensorModule.coe_lTensor
-- 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)
⊢ ∀ ⦃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:
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, Membership.mem, Subtype, Submodule.subtype, TensorProduct, DFunLike.coe, injective_of_isLocalized_span, TensorProduct.AlgebraTensorModule.lTensor
-- 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)
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)

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

Premises used: IsLocalizedModule.map_lTensor
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
S : Type u_2
inst : CommSemiring S
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : Module S M
s : Set S
spn : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ (r : (↑s : Type u_2)), Flat S (LocalizedModule.Away (↑r : S) M)
⊢ Flat S M

Tactic:
flat_of_isLocalized_span _ _ _ spn _ (fun _ ↦ mkLinearMap _ _) h

Premises used: Module.flat_of_isLocalized_span, LocalizedModule.mkLinearMap
-- 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
p_1 : Submonoid R
inst_3 : IsLocalization p_1 S
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
A : Type u_4
B : Type u_5
inst_8 : CommRing A
inst_9 : CommRing B
inst_10 : Algebra A B
inst_11 : Module.Flat A B
p : Ideal A
inst_12 : p.IsPrime
P : Ideal B
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
inst_15 : Algebra.{u_4, u_5} (Localization.AtPrime p) (Localization.AtPrime P)
inst_16 : Localization.AtPrime.IsLiesOverAlgebra p P
rw : Module.Flat.{u_4, u_5} A (Localization.AtPrime P)
⊢ Module.Flat.{u_4, u_5} (Localization.AtPrime p) (Localization.AtPrime P)

Tactic:
rw [Module.flat_iff_of_isLocalization (Localization.AtPrime p) p.primeCompl]

Premises used: Localization.AtPrime, Ideal.primeCompl, Module.flat_iff_of_isLocalization
-- 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
p_1 : Submonoid R
inst_3 : IsLocalization p_1 S
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
A : Type u_4
B : Type u_5
inst_8 : CommRing A
inst_9 : CommRing B
inst_10 : Algebra A B
inst_11 : Module.Flat A B
p : Ideal A
inst_12 : p.IsPrime
P : Ideal B
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
inst_15 : Algebra.{u_4, u_5} (Localization.AtPrime p) (Localization.AtPrime P)
inst_16 : Localization.AtPrime.IsLiesOverAlgebra p P
⊢ Module.Flat.{u_4, u_5} A (Localization.AtPrime P)

Tactic:
Module.Flat.trans A B (Localization.AtPrime P)

Premises used: Localization.AtPrime, Module.Flat.trans