awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : FaithfullyFlat R S
H : Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
have this : Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
  ((↑R :
      {S : Type u_2} →
        {M : Type (max u_1 u_2)} →
          {M₂ : Type (max u_2 u_3)} →
            [inst : Semiring R] →
              [inst_6 : Semiring S] →
                [inst_7 : AddCommMonoid M] →
                  [inst_8 : AddCommMonoid M₂] →
                    [inst_9 : Module R M] →
                      [inst_10 : Module R M₂] →
                        [inst_11 : Module S M] →
                          [inst_12 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S ⊗[R] T))
Tactic: have : LinearMap.lTensor S (Algebra.linearMap R T) =
      Algebra.linearMap S (S ⊗[R] T) ∘ₗ (AlgebraTensorModule.rid R S S).toLinearMap := by
    ext; simp
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : FaithfullyFlat R S
H : Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
this :
  Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_2 u_3)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
        S ⊗[R] R →ₗ[S] S ⊗[R] T))
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
have apply : Function.Injective (α := S ⊗[R] R) (β := S ⊗[R] T)
  (⇑(LinearMap.lTensor S (Algebra.linearMap R T)) : (a : S ⊗[R] R) → S ⊗[R] T)
Tactic: apply (Module.FaithfullyFlat.lTensor_injective_iff_injective R S (Algebra.linearMap R T)).mp
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_2 u_3)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
        S ⊗[R] R →ₗ[S] S ⊗[R] T))
have a : ∀ (x : S),
  Eq (α := S ⊗[R] T)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R T)) : S →ₗ[R] R →ₗ[R] S ⊗[R] T) :
              (a : S) → R →ₗ[R] S ⊗[R] T)
            x :
          R →ₗ[R] S ⊗[R] T) :
        (a : R) → S ⊗[R] T)
      1)
    (((((AlgebraTensorModule.curry
                  ((↑R :
                      {S : Type u_2} →
                        {M : Type (max u_1 u_2)} →
                          {M₂ : Type (max u_2 u_3)} →
                            [inst : Semiring R] →
                              [inst_6 : Semiring S] →
                                [inst_7 : AddCommMonoid M] →
                                  [inst_8 : AddCommMonoid M₂] →
                                    [inst_9 : Module R M] →
                                      [inst_10 : Module R M₂] →
                                        [inst_11 : Module S M] →
                                          [inst_12 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
                      S ⊗[R] R →ₗ[S] S ⊗[R] T)) :
                S →ₗ[R] R →ₗ[R] S ⊗[R] T) :
              (a : S) → R →ₗ[R] S ⊗[R] T)
            x :
          R →ₗ[R] S ⊗[R] T) :
        (a : R) → S ⊗[R] T)
      1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Descent (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
have this : Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
  ((↑R :
      {S : Type u_2} →
        {M : Type (max u_1 u_2)} →
          {M₂ : Type (max u_2 u_3)} →
            [inst : Semiring R] →
              [inst_6 : Semiring S] →
                [inst_7 : AddCommMonoid M] →
                  [inst_8 : AddCommMonoid M₂] →
                    [inst_9 : Module R M] →
                      [inst_10 : Module R M₂] →
                        [inst_11 : Module S M] →
                          [inst_12 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S ⊗[R] T))
Tactic: have : LinearMap.lTensor S (Algebra.linearMap R T) =
      Algebra.linearMap S (S ⊗[R] T) ∘ₗ (AlgebraTensorModule.rid R S S).toLinearMap := by
    ext; simp
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Descent (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
this :
  Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_2 u_3)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
        S ⊗[R] R →ₗ[S] S ⊗[R] T))
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
have apply : Function.Surjective (α := S ⊗[R] R) (β := S ⊗[R] T)
  (⇑(LinearMap.lTensor S (Algebra.linearMap R T)) : (a : S ⊗[R] R) → S ⊗[R] T)
Tactic: apply (Module.FaithfullyFlat.lTensor_surjective_iff_surjective R S (Algebra.linearMap R T)).mp
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Descent (goal)
Goal:
⊢ CodescendsAlong.{u_1}
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat
have apply : ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  FaithfullyFlat (algebraMap R S) →
    Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T) →
      Function.Injective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
Tactic: apply CodescendsAlong.mk _ injective_respectsIso
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Descent (hypothesis)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
H : Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Function.Injective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
have h₁ : Module.FaithfullyFlat R S
Tactic: rw [faithfullyFlat_algebraMap_iff] at h
Cleared hypotheses: h, H
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Descent (goal)
Goal:
⊢ CodescendsAlong.{u_1}
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S))
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat
have apply : ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  FaithfullyFlat (algebraMap R S) →
    Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T) →
      Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
Tactic: apply CodescendsAlong.mk _ surjective_respectsIso
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Descent (hypothesis)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
have h₁ : Module.FaithfullyFlat R S
Tactic: rw [faithfullyFlat_algebraMap_iff] at h
Cleared hypotheses: h, H
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (goal)
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
⊢ Module.Flat R S
have refine : ∀ (P : Type u_1) (x : AddCommMonoid P) (x_1 : Module R P) (N : Submodule R P),
  Function.Injective (α := S ⊗[R] ↥N) (β := S ⊗[R] P) (⇑(lTensor S N.subtype) : (a : S ⊗[R] ↥N) → S ⊗[R] P)
Tactic: refine Module.Flat.iff_lTensor_injectiveₛ.mpr fun P _ _ N ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (hypothesis)
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
⊢ Function.Injective (α := S ⊗[R] ↥N) (β := S ⊗[R] P) (⇑(lTensor S N.subtype) : (a : S ⊗[R] ↥N) → S ⊗[R] P)
have 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)
Tactic: have h := ((range N.subtype).isLocalizedModule S p (TensorProduct.mk R S P 1)).isBaseChange _ S
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (goal)
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))
have a : ∀ (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)
    (((((AlgebraTensorModule.curry
                    (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))) :
                  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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (goal)
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)
    (((((AlgebraTensorModule.curry
                    (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))) :
                  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)
have a : 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 sorry)) : 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: change _ = (h.equiv _).1
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (hypothesis)
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
⊢ Function.Injective (α := S ⊗[R] ↥N) (β := S ⊗[R] P) (⇑(lTensor S N.subtype) : (a : S ⊗[R] ↥N) → S ⊗[R] P)
have 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))
Tactic: have : N.subtype.lTensor S = Submodule.subtype _ ∘ₗ e.toLinearMap := by
    ext; change _ = (h.equiv _).1; simp [h.equiv_tmul, TensorProduct.smul_tmul']
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (goal)
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)
⊢ Flat R M
have 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)
Tactic: simp_rw [Flat.iff_lTensor_injectiveₛ] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (goal)
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) (⇑(lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)
have 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)
Tactic: simp_rw [← AlgebraTensorModule.coe_lTensor (A := S)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (goal)
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)
⊢ Flat R M
have 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)
Tactic: simp_rw [Flat.iff_lTensor_injectiveₛ] at H ⊢
Cleared hypotheses: H