awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
⊢ f = 0
have rw : Eq (α := M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
  (lTensor M (AlgebraTensorModule.map LinearMap.id f) : M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
  (0 : M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
Tactic: rw [zero_iff_lTensor_zero (R:= R) (M := S) f,
    show f.lTensor S = (AlgebraTensorModule.map (A:= S) LinearMap.id f).restrictScalars R by aesop,
    show (0 :  S ⊗[R] N →ₗ[R] S ⊗[R] N') = (0 : S ⊗[R] N →ₗ[S] S ⊗[R] N').restrictScalars R by rfl,
    restrictScalars_inj, zero_iff_lTensor_zero (R:= S) (M := M)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
⊢ Eq (α := M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
    (lTensor M (AlgebraTensorModule.map LinearMap.id f) : M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
    (0 : M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
have a : ∀ (m : M) (n : N),
  Eq (α := M ⊗[S] (S ⊗[R] N'))
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry (lTensor M (AlgebraTensorModule.map LinearMap.id f)) :
                        M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                      (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                    m) :
                S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
              (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
            1 :
          (a : N) → M ⊗[S] (S ⊗[R] N'))
        n :
      M ⊗[S] (S ⊗[R] N'))
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry 0 : M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                      (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                    m) :
                S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
              (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
            1 :
          (a : N) → M ⊗[S] (S ⊗[R] N'))
        n :
      M ⊗[S] (S ⊗[R] N'))
Tactic: ext m n
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
m : M
n : N
⊢ Eq (α := M ⊗[S] (S ⊗[R] N'))
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry (lTensor M (AlgebraTensorModule.map LinearMap.id f)) :
                        M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                      (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                    m) :
                S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
              (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
            1 :
          (a : N) → M ⊗[S] (S ⊗[R] N'))
        n :
      M ⊗[S] (S ⊗[R] N'))
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry 0 : M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                      (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                    m) :
                S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
              (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
            1 :
          (a : N) → M ⊗[S] (S ⊗[R] N'))
        n :
      M ⊗[S] (S ⊗[R] N'))
have a : Eq (α := M ⊗[R] N')
  (((AlgebraTensorModule.cancelBaseChange R S S M N' : M ⊗[S] (S ⊗[R] N') ≃ₗ[S] M ⊗[R] N') :
        (a : M ⊗[S] (S ⊗[R] N')) → M ⊗[R] N')
      ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry (lTensor M (AlgebraTensorModule.map LinearMap.id f)) :
                        M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                      (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                    m) :
                S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
              (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
            1 :
          (a : N) → M ⊗[S] (S ⊗[R] N'))
        n) :
    M ⊗[R] N')
  (((AlgebraTensorModule.cancelBaseChange R S S M N' : M ⊗[S] (S ⊗[R] N') ≃ₗ[S] M ⊗[R] N') :
        (a : M ⊗[S] (S ⊗[R] N')) → M ⊗[R] N')
      ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry 0 : M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                      (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                    m) :
                S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
              (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
            1 :
          (a : N) → M ⊗[S] (S ⊗[R] N'))
        n) :
    M ⊗[R] N')
Tactic: apply_fun AlgebraTensorModule.cancelBaseChange R S S M N' using LinearEquiv.injective _
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 M
⊢ FaithfullyFlat S (S ⊗[R] M)
have rw : Flat S (S ⊗[R] M) ∧
  ∀ (N : Type (max u_1 v)) [inst_6 : AddCommGroup N] [inst_7 : Module S N],
    Subsingleton (N ⊗[S] (S ⊗[R] M)) → Subsingleton N
Tactic: rw [Module.FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 M
⊢ Flat S (S ⊗[R] M) ∧
    ∀ (N : Type (max u_1 v)) [inst_6 : AddCommGroup N] [inst_7 : Module S N],
      Subsingleton (N ⊗[S] (S ⊗[R] M)) → Subsingleton N
have refine : ∀ (N : Type (max u_1 v)) (x : AddCommGroup N) (x_1 : Module S N) (hN : Subsingleton (N ⊗[S] (S ⊗[R] M))), Subsingleton N
Tactic: refine ⟨inferInstance, fun N _ _ hN ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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 M
N : Type (max u_1 v)
x : AddCommGroup N
x_1 : Module S N
hN : Subsingleton (N ⊗[S] (S ⊗[R] M))
x_2 : Module R N := compHom N (algebraMap R S)
⊢ Subsingleton N
have this : IsScalarTower R S N
Tactic: have : IsScalarTower R S N := IsScalarTower.of_algebraMap_smul fun r ↦ congrFun rfl
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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 M
N : Type (max u_1 v)
x : AddCommGroup N
x_1 : Module S N
hN : Subsingleton (N ⊗[S] (S ⊗[R] M))
x_2 : Module R N := compHom N (algebraMap R S)
this : IsScalarTower R S N
⊢ Subsingleton N
have this₁ : Subsingleton (N ⊗[R] M)
Tactic: have := (AlgebraTensorModule.cancelBaseChange R S S N M).symm.subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ Flat R M
have 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')
Tactic: rw [Module.Flat.iff_lTensor_preserves_injective_linearMap]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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)
⊢ Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
have this : Flat R (S ⊗[R] M)
Tactic: have : Flat R (S ⊗[R] M) := Flat.trans _ S _
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)
have 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))
Tactic: rw [← FaithfullyFlat.lTensor_injective_iff_injective R S]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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)
⊢ 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))
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
have refine : ∀ (h : LE.le (α := Submodule A (A ⊗[R] M)) (baseChange A p) (baseChange A q)), p ≤ q
Tactic: refine ⟨fun h ↦ ?_, baseChange_mono A⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ p ≤ q
have rwa : p ≤ q.mkQ.ker
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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
⊢ p ≤ q
have rwa₁ : q.mkQ ∘ₗ p.subtype = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
⊢ p ≤ q
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
⊢ p ≤ q
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
⊢ p ≤ q
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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))
⊢ p ≤ q
have rwa₅ : LE.le (α := Submodule R (A ⊗[R] M)) (range (lTensor A p.subtype)) (range (lTensor A q.subtype))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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))
⊢ p ≤ q
have rwa₆ : LE.le (α := Submodule R (A ⊗[R] M)) (restrictScalars R (range (lTensor A p.subtype)))
  (restrictScalars R (range (lTensor A q.subtype)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ IsNoetherian R M
have rw : ∀ (h : WellFoundedGT (Submodule A (A ⊗[R] M))), WellFoundedGT.{u_2} (Submodule R M)
Tactic: rw [isNoetherian_iff'] at h ⊢
Cleared hypotheses: h
-- 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)
⊢ 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