awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
N : Type u_2
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : AddCommGroup N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
I : Ideal R
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal S) (β := Submodule S N) (Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤ ≠ ⊤ ↔
    HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤

Tactic:
simpa only [← Submodule.Quotient.subsingleton_iff.not] using not_congr <|
    (tensorQuotEquivQuotSMul N (I.map (algebraMap R S))).symm ≪≫ₗ TensorProduct.comm S N _ ≪≫ₗ
      hf.tensorEquiv _ ≪≫ₗ AlgebraTensorModule.congr (I.qoutMapEquivTensorQout S) (.refl R M) ≪≫ₗ
        AlgebraTensorModule.assoc R R S S _ M ≪≫ₗ (TensorProduct.comm R _ M).baseChange R S _ _ ≪≫ₗ
          (tensorQuotEquivQuotSMul M I).baseChange R S _ _ |>.subsingleton_congr.trans <|
            subsingleton_tensorProduct_iff_right R S

Premises used: LinearEquiv.symm, TensorProduct.comm, Algebra.algebraMap, Ideal.qoutMapEquivTensorQout, Module.FaithfullyFlat.subsingleton_tensorProduct_iff_right, Equiv.subsingleton_congr, Ideal.map, Iff.not, LinearEquiv.toAddEquiv, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.baseChange, Iff.trans, LinearEquiv.refl, Submodule.Quotient.subsingleton_iff, AddEquiv.toEquiv, TensorProduct.tensorQuotEquivQuotSMul, LinearEquiv.trans, IsBaseChange.tensorEquiv, not_congr, TensorProduct.AlgebraTensorModule.assoc
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
rw :
  ∀ ⦃N N' : Type (max u v)⦄ [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup N'] [inst_9 : Module R N]
    [inst_10 : Module R N'] (f : N →ₗ[R] N'),
    Function.Injective (α := N) (β := N') (⇑f : (a : N) → N') →
      Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
⊢ Flat R M

Tactic:
rw [Module.Flat.iff_lTensor_preserves_injective_linearMap]

Premises used: Module.Flat.iff_lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
_ :
  ∀ [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P] (f : N →ₗ[R] P),
    Function.Injective (α := N) (β := P) (⇑f : (a : N) → P) →
      Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
⊢ ∀ [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P] (f : N →ₗ[R] P),
    Function.Injective (α := N) (β := P) (⇑f : (a : N) → P) →
      Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)

Tactic:
_
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst_7 : AddCommGroup N
_ :
  ∀ [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P] (f : N →ₗ[R] P),
    Function.Injective (α := N) (β := P) (⇑f : (a : N) → P) →
      Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
⊢ ∀ [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P] (f : N →ₗ[R] P),
    Function.Injective (α := N) (β := P) (⇑f : (a : N) → P) →
      Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)

Tactic:
_
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
_ :
  ∀ [inst_9 : Module R N] [inst_10 : Module R P] (f : N →ₗ[R] P),
    Function.Injective (α := N) (β := P) (⇑f : (a : N) → P) →
      Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
⊢ ∀ [inst_9 : Module R N] [inst_10 : Module R P] (f : N →ₗ[R] P),
    Function.Injective (α := N) (β := P) (⇑f : (a : N) → P) →
      Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)

Tactic:
_
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
_ :
  ∀ [inst_10 : Module R P] (f : N →ₗ[R] P),
    Function.Injective (α := N) (β := P) (⇑f : (a : N) → P) →
      Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
⊢ ∀ [inst_10 : Module R P] (f : N →ₗ[R] P),
    Function.Injective (α := N) (β := P) (⇑f : (a : N) → P) →
      Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)

Tactic:
_
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
hf : Function.Injective (α := N) (β := P) (⇑f : (a : N) → P)
⊢ Flat R (S ⊗[R] M)

Tactic:
have : Flat R (S ⊗[R] M) := Flat.trans _ S _
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
hf : Function.Injective (α := N) (β := P) (⇑f : (a : N) → P)
this : Flat R (S ⊗[R] M)
rw :
  Function.Injective (α := S ⊗[R] (M ⊗[R] N)) (β := S ⊗[R] (M ⊗[R] P))
    (⇑(LinearMap.lTensor S (LinearMap.lTensor M f)) : (a : S ⊗[R] (M ⊗[R] N)) → S ⊗[R] (M ⊗[R] P))
⊢ Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)

Tactic:
rw [← FaithfullyFlat.lTensor_injective_iff_injective R S]

Premises used: Module.FaithfullyFlat.lTensor_injective_iff_injective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
hf : Function.Injective (α := N) (β := P) (⇑f : (a : N) → P)
this : Flat R (S ⊗[R] M)
a :
  ∀ (x : S) (x_1 : M) (x_2 : N),
    Eq (α := S ⊗[R] (M ⊗[R] P))
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry (LinearMap.lTensor S (LinearMap.lTensor M f)) :
                            S →ₗ[R] M ⊗[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
                          (a : S) → M ⊗[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P))
                        x) :
                    M →ₗ[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
                  (a : M) → N →ₗ[R] S ⊗[R] (M ⊗[R] P))
                x_1 :
              N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
            (a : N) → S ⊗[R] (M ⊗[R] P))
          x_2 :
        S ⊗[R] (M ⊗[R] P))
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.curry
                              ((↑(TensorProduct.assoc R S M P) : S ⊗[R] M ⊗[R] P →ₗ[R] S ⊗[R] (M ⊗[R] P)) ∘ₗ
                                LinearMap.lTensor (S ⊗[R] M) f ∘ₗ
                                  (↑(LinearEquiv.symm (TensorProduct.assoc R S M N)) :
                                    S ⊗[R] (M ⊗[R] N) →ₗ[R] S ⊗[R] M ⊗[R] N)) :
                            S →ₗ[R] M ⊗[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
                          (a : S) → M ⊗[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P))
                        x) :
                    M →ₗ[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
                  (a : M) → N →ₗ[R] S ⊗[R] (M ⊗[R] P))
                x_1 :
              N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
            (a : N) → S ⊗[R] (M ⊗[R] P))
          x_2 :
        S ⊗[R] (M ⊗[R] P))
⊢ Eq (α := S ⊗[R] (M ⊗[R] N) →ₗ[R] S ⊗[R] (M ⊗[R] P)) (LinearMap.lTensor S (LinearMap.lTensor M f))
    ((↑(TensorProduct.assoc R S M P) : S ⊗[R] M ⊗[R] P →ₗ[R] S ⊗[R] (M ⊗[R] P)) ∘ₗ
      LinearMap.lTensor (S ⊗[R] M) f ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.assoc R S M N)) : S ⊗[R] (M ⊗[R] N) →ₗ[R] S ⊗[R] M ⊗[R] N))

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
hf : Function.Injective (α := N) (β := P) (⇑f : (a : N) → P)
this : Flat R (S ⊗[R] M)
x : S
x_1 : M
x_2 : N
⊢ Eq (α := S ⊗[R] (M ⊗[R] P))
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry (LinearMap.lTensor S (LinearMap.lTensor M f)) :
                          S →ₗ[R] M ⊗[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
                        (a : S) → M ⊗[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P))
                      x) :
                  M →ₗ[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
                (a : M) → N →ₗ[R] S ⊗[R] (M ⊗[R] P))
              x_1 :
            N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
          (a : N) → S ⊗[R] (M ⊗[R] P))
        x_2 :
      S ⊗[R] (M ⊗[R] P))
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry
                            ((↑(TensorProduct.assoc R S M P) : S ⊗[R] M ⊗[R] P →ₗ[R] S ⊗[R] (M ⊗[R] P)) ∘ₗ
                              LinearMap.lTensor (S ⊗[R] M) f ∘ₗ
                                (↑(LinearEquiv.symm (TensorProduct.assoc R S M N)) :
                                  S ⊗[R] (M ⊗[R] N) →ₗ[R] S ⊗[R] M ⊗[R] N)) :
                          S →ₗ[R] M ⊗[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
                        (a : S) → M ⊗[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P))
                      x) :
                  M →ₗ[R] N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
                (a : M) → N →ₗ[R] S ⊗[R] (M ⊗[R] P))
              x_1 :
            N →ₗ[R] S ⊗[R] (M ⊗[R] P)) :
          (a : N) → S ⊗[R] (M ⊗[R] P))
        x_2 :
      S ⊗[R] (M ⊗[R] P))

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
hf : Function.Injective (α := N) (β := P) (⇑f : (a : N) → P)
this : Flat R (S ⊗[R] M)
⊢ Eq (α := S ⊗[R] (M ⊗[R] N) →ₗ[R] S ⊗[R] (M ⊗[R] P)) (LinearMap.lTensor S (LinearMap.lTensor M f))
    ((↑(TensorProduct.assoc R S M P) : S ⊗[R] M ⊗[R] P →ₗ[R] S ⊗[R] (M ⊗[R] P)) ∘ₗ
      LinearMap.lTensor (S ⊗[R] M) f ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.assoc R S M N)) : S ⊗[R] (M ⊗[R] N) →ₗ[R] S ⊗[R] M ⊗[R] N))

Tactic:
have : LinearMap.lTensor S (LinearMap.lTensor M f) =
      (TensorProduct.assoc _ _ _ _).toLinearMap ∘ₗ LinearMap.lTensor (S ⊗[R] M) f ∘ₗ
        (TensorProduct.assoc _ _ _ _).symm.toLinearMap := by
    ext
    simp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
inst_6 : Flat S (S ⊗[R] M)
N P : Type (max u v)
inst_7 : AddCommGroup N
inst_8 : AddCommGroup P
inst_9 : Module R N
inst_10 : Module R P
f : N →ₗ[R] P
hf : Function.Injective (α := N) (β := P) (⇑f : (a : N) → P)
this_1 : Flat R (S ⊗[R] M)
this :
  Eq (α := S ⊗[R] (M ⊗[R] N) →ₗ[R] S ⊗[R] (M ⊗[R] P)) (LinearMap.lTensor S (LinearMap.lTensor M f))
    ((↑(TensorProduct.assoc R S M P) : S ⊗[R] M ⊗[R] P →ₗ[R] S ⊗[R] (M ⊗[R] P)) ∘ₗ
      LinearMap.lTensor (S ⊗[R] M) f ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.assoc R S M N)) : S ⊗[R] (M ⊗[R] N) →ₗ[R] S ⊗[R] M ⊗[R] N))
⊢ Function.Injective (α := S ⊗[R] (M ⊗[R] N)) (β := S ⊗[R] (M ⊗[R] P))
    (⇑(LinearMap.lTensor S (LinearMap.lTensor M f)) : (a : S ⊗[R] (M ⊗[R] N)) → S ⊗[R] (M ⊗[R] P))

Tactic:
simpa [this] using Flat.lTensor_preserves_injective_linearMap f hf

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R S
⊢ Flat S (S ⊗[R] M) ↔ Flat R M

Tactic:
⟨fun _ ↦ .of_flat_tensorProduct R M S, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Module.Flat.of_flat_tensorProduct, Iff.intro
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FaithfullyFlat R A
inst_4 : AddCommGroup M
inst_5 : Module R M
p q : Submodule R M
⊢ LE.le (α := Submodule A (A ⊗[R] M)) (baseChange A p) (baseChange A q) ↔ p ≤ q

Tactic:
⟨fun h ↦ ?_, baseChange_mono A⟩

Premises used: Submodule.baseChange_mono, Iff.intro
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FaithfullyFlat R A
inst_4 : AddCommGroup M
inst_5 : Module R M
p q : Submodule R M
refine : ∀ (h : LE.le (α := Submodule A (A ⊗[R] M)) (baseChange A p) (baseChange A q)), p ≤ q
⊢ LE.le (α := Submodule A (A ⊗[R] M)) (baseChange A p) (baseChange A q) ↔ p ≤ q

Tactic:
refine ⟨fun h ↦ ?_, baseChange_mono A⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FaithfullyFlat R A
inst_4 : AddCommGroup M
inst_5 : Module R M
p q : Submodule R M
h : LE.le (α := Submodule A (A ⊗[R] M)) (baseChange A p) (baseChange A q)
rwa : p ≤ q.mkQ.ker
rwa₁ : q.mkQ ∘ₗ p.subtype = 0
rwa₂ :
  Eq (α := TensorProduct.{u_1, u_3, u_2} R A ↥p →ₗ[R] TensorProduct.{u_1, u_3, u_2} R A (M ⧸ q))
    (lTensor A (q.mkQ ∘ₗ p.subtype)) 0
rwa₃ :
  Eq (α := TensorProduct.{u_1, u_3, u_2} R A ↥p →ₗ[R] TensorProduct.{u_1, u_3, u_2} R A (M ⧸ q))
    (lTensor A q.mkQ ∘ₗ lTensor A p.subtype) 0
rwa₄ :
  LE.le (α := Submodule R (A ⊗[R] M)) (range (lTensor A p.subtype))
    (ker (M₂ := TensorProduct.{u_1, u_3, u_2} R A (M ⧸ q)) (lTensor A q.mkQ))
rwa₅ : LE.le (α := Submodule R (A ⊗[R] M)) (range (lTensor A p.subtype)) (range (lTensor A q.subtype))
rwa₆ rwa₇ rwa₈ rwa₉ :
  LE.le (α := Submodule R (A ⊗[R] M)) (restrictScalars R (range (lTensor A p.subtype)))
    (restrictScalars R (range (lTensor A q.subtype)))
⊢ p ≤ q

Tactic:
rwa [← q.ker_mkQ, le_ker_iff_comp_subtype_eq_zero, FaithfullyFlat.zero_iff_lTensor_zero R A,
    lTensor_comp, ← range_le_ker_iff, lTensor_mkQ, ← restrictScalars_le R]

Premises used: LinearMap.le_ker_iff_comp_subtype_eq_zero, Submodule.restrictScalars_le, Module.FaithfullyFlat.zero_iff_lTensor_zero, Submodule.ker_mkQ, LinearMap.lTensor_comp, LinearMap.range_le_ker_iff, lTensor_mkQ
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FaithfullyFlat R A
inst_4 : AddCommGroup M
inst_5 : Module R M
p q : Submodule R M
⊢ Eq (α := Submodule A (A ⊗[R] M)) (baseChange A p) (baseChange A q) ↔ p = q

Tactic:
simp [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FaithfullyFlat R A
inst_4 : AddCommGroup M
inst_5 : Module R M
p q : Submodule R M
h : Eq (α := Submodule A (A ⊗[R] M)) (baseChange A p) (baseChange A q)
⊢ p = q

Tactic:
baseChange_inj.mp h

Premises used: Submodule.baseChange_inj, Iff.mp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FaithfullyFlat R A
inst_4 : AddCommGroup M
inst_5 : Module R M
h : IsNoetherian A (A ⊗[R] M)
rw : ∀ (h : WellFoundedGT (Submodule A (A ⊗[R] M))), WellFoundedGT.{u_2} (Submodule R M)
⊢ IsNoetherian R M

Tactic:
rw [isNoetherian_iff'] at h ⊢

Premises used: isNoetherian_iff'
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FaithfullyFlat R A
inst_4 : AddCommGroup M
inst_5 : Module R M
h : WellFoundedGT (Submodule A (A ⊗[R] M))
⊢ WellFoundedGT.{u_2} (Submodule R M)

Tactic:
(baseChangeOrderEmbedding R M A).wellFoundedGT

Premises used: Submodule.baseChangeOrderEmbedding, OrderEmbedding.wellFoundedGT
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FaithfullyFlat R A
inst_4 : AddCommGroup M
inst_5 : Module R M
h : WellFoundedGT (Submodule A (A ⊗[R] M))
⊢ WellFoundedGT.{u_2} (Submodule R M)

Tactic:
exact (baseChangeOrderEmbedding R M A).wellFoundedGT

Premises used: Submodule.baseChangeOrderEmbedding, OrderEmbedding.wellFoundedGT
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : FaithfullyFlat R A
inst_4 : AddCommGroup M
inst_5 : Module R M
h : IsArtinian A (A ⊗[R] M)
⊢ IsArtinian R M

Tactic:
(baseChangeOrderEmbedding R M A).wellFoundedLT

Premises used: Submodule.baseChangeOrderEmbedding, OrderEmbedding.wellFoundedLT
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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)
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)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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)
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:
simp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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)
⊢ 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