-- Mathlib/RingTheory/Flat/Localization.lean
theorem IsLocalization.flat : Module.Flat R S

Proof state:
case a.h.h
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝³ : AddCommMonoid P
x✝² : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) (range N.subtype)) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
x✝¹ : S
x✝ : ↥N
⊢ ((AlgebraTensorModule.curry (lTensor S N.subtype)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((Submodule.localized₀ p ((TensorProduct.mk R S P) 1) (range N.subtype)).subtype ∘ₗ ↑e))
        x✝¹)
      x✝

Tactic:
show _ = (h.equiv _).1

Result:
case a.h.h
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝³ : AddCommMonoid P
x✝² : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) (range N.subtype)) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
x✝¹ : S
x✝ : ↥N
⊢ ((AlgebraTensorModule.curry (lTensor S N.subtype)) x✝¹) x✝ =
    ↑(h.equiv (↑(LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯)) (((TensorProduct.mk R S ↥N) x✝¹) x✝)))

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) (range N.subtype)) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
⊢ Function.Injective ⇑(lTensor S N.subtype)

Tactic:
have : N.subtype.lTensor S = Submodule.subtype _ ∘ₗ e.toLinearMap := by
  ext; show _ = (h.equiv _).1; simp [h.equiv_tmul, TensorProduct.smul_tmul']

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) (range N.subtype)) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
this : lTensor S N.subtype = (Submodule.localized₀ p ((TensorProduct.mk R S P) 1) (range N.subtype)).subtype ∘ₗ ↑e
⊢ Function.Injective ⇑(lTensor S N.subtype)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
⊢ Function.Injective ⇑(lTensor S N.subtype)

Tactic:
have h := ((range N.subtype).isLocalizedModule S p (TensorProduct.mk R S P 1)).isBaseChange _ S

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
⊢ Function.Injective ⇑(lTensor S N.subtype)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) (range N.subtype)) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
⊢ lTensor S N.subtype = (Submodule.localized₀ p ((TensorProduct.mk R S P) 1) (range N.subtype)).subtype ∘ₗ ↑e

Tactic:
ext

Result:
case a.h.h
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝³ : AddCommMonoid P
x✝² : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) (range N.subtype)) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
x✝¹ : S
x✝ : ↥N
⊢ ((AlgebraTensorModule.curry (lTensor S N.subtype)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((Submodule.localized₀ p ((TensorProduct.mk R S P) 1) (range N.subtype)).subtype ∘ₗ ↑e))
        x✝¹)
      x✝

Proof state:
case a.h.h
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝³ : AddCommMonoid P
x✝² : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) (range N.subtype)) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
x✝¹ : S
x✝ : ↥N
⊢ ((AlgebraTensorModule.curry (lTensor S N.subtype)) x✝¹) x✝ =
    ↑(h.equiv (↑(LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯)) (((TensorProduct.mk R S ↥N) x✝¹) x✝)))

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

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
⊢ Function.Injective ⇑(lTensor S N.subtype)

Tactic:
let e := (LinearEquiv.ofInjective _ Subtype.val_injective).lTensor S ≪≫ₗ h.equiv.restrictScalars R

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) (range N.subtype)) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
⊢ Function.Injective ⇑(lTensor S N.subtype)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
⊢ Module.Flat R S

Tactic:
refine Module.Flat.iff_lTensor_injectiveₛ.mpr fun P _ _ N ↦ ?_

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
⊢ Function.Injective ⇑(lTensor S N.subtype)