awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
N1 : Type u_1
inst_3 : AddCommGroup N1
inst_4 : Module R N1
N2 : Type u_2
inst_5 : AddCommGroup N2
inst_6 : Module R N2
N3 : Type u_3
inst_7 : AddCommGroup N3
inst_8 : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex :
  Function.Exact (M := M ⊗[R] N1) (N := M ⊗[R] N2) (P := M ⊗[R] N3)
    (⇑(LinearMap.lTensor M l12) : (a : M ⊗[R] N1) → M ⊗[R] N2)
    (⇑(LinearMap.lTensor M l23) : (a : M ⊗[R] N2) → M ⊗[R] N3)
⊢ Eq (α := M ⊗[R] N2 →ₗ[R] N3 ⊗[R] M)
    (LinearMap.rTensor M l23 ∘ₗ (↑(TensorProduct.comm R M N2) : M ⊗[R] N2 →ₗ[R] N2 ⊗[R] M))
    ((↑(TensorProduct.comm R M N3) : M ⊗[R] N3 →ₗ[R] N3 ⊗[R] M) ∘ₗ LinearMap.lTensor M l23)
have a : ∀ (x : M) (x_1 : N2),
  Eq (α := N3 ⊗[R] M)
    (((((AlgebraTensorModule.curry
                    (LinearMap.rTensor M l23 ∘ₗ (↑(TensorProduct.comm R M N2) : M ⊗[R] N2 →ₗ[R] N2 ⊗[R] M)) :
                  M →ₗ[R] N2 →ₗ[R] N3 ⊗[R] M) :
                (a : M) → N2 →ₗ[R] N3 ⊗[R] M)
              x :
            N2 →ₗ[R] N3 ⊗[R] M) :
          (a : N2) → N3 ⊗[R] M)
        x_1 :
      N3 ⊗[R] M)
    (((((AlgebraTensorModule.curry
                    ((↑(TensorProduct.comm R M N3) : M ⊗[R] N3 →ₗ[R] N3 ⊗[R] M) ∘ₗ LinearMap.lTensor M l23) :
                  M →ₗ[R] N2 →ₗ[R] N3 ⊗[R] M) :
                (a : M) → N2 →ₗ[R] N3 ⊗[R] M)
              x :
            N2 →ₗ[R] N3 ⊗[R] M) :
          (a : N2) → N3 ⊗[R] M)
        x_1 :
      N3 ⊗[R] M)
Tactic: ext
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
⊢ Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Injective.{u_4 + 1, u_5 + 1} (α := N) (β := N') (⇑f : (a : N) → N')
have rw : Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N') (⇑0 : (a : M ⊗[R] Unit) → M ⊗[R] N)
    (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
  Function.Exact.{0, u_4, u_5} (M := Unit) (N := N) (P := N') (⇑0 : (a : Unit) → N) (⇑f : (a : N) → N')
Tactic: rw [← LinearMap.exact_zero_iff_injective (M ⊗[R] Unit), ← LinearMap.exact_zero_iff_injective Unit]
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
| Function.Exact.{0, u_4, u_5} (M := Unit) (N := N) (P := N') (⇑0 : (a : Unit) → N) (⇑f : (a : N) → N')
have rw : Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N')
  (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] Unit) → M ⊗[R] N) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
Tactic: rw [← lTensor_exact_iff_exact R M]
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
⊢ Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N') (⇑0 : (a : M ⊗[R] Unit) → M ⊗[R] N)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Exact.{0, u_4, u_5} (M := Unit) (N := N) (P := N') (⇑0 : (a : Unit) → N) (⇑f : (a : N) → N')
have conv_rhs : Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N') (⇑0 : (a : M ⊗[R] Unit) → M ⊗[R] N)
    (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
  Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N')
    (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] Unit) → M ⊗[R] N) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
Tactic: conv_rhs => rw [← lTensor_exact_iff_exact R M]
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
⊢ Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Surjective.{u_4 + 1, u_5 + 1} (α := N) (β := N') (⇑f : (a : N) → N')
have rw : Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
    (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑0 : (a : M ⊗[R] N') → M ⊗[R] Unit) ↔
  Function.Exact.{u_4, u_5, 0} (M := N) (N := N') (P := Unit) (⇑f : (a : N) → N') (⇑0 : (a : N') → Unit)
Tactic: rw [← LinearMap.exact_zero_iff_surjective (M ⊗[R] Unit),
    ← LinearMap.exact_zero_iff_surjective Unit]
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
| Function.Exact.{u_4, u_5, 0} (M := N) (N := N') (P := Unit) (⇑f : (a : N) → N') (⇑0 : (a : N') → Unit)
have rw : Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
  (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] N') → M ⊗[R] Unit)
Tactic: rw [← lTensor_exact_iff_exact R M]
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑0 : (a : M ⊗[R] N') → M ⊗[R] Unit) ↔
    Function.Exact.{u_4, u_5, 0} (M := N) (N := N') (P := Unit) (⇑f : (a : N) → N') (⇑0 : (a : N') → Unit)
have conv_rhs : Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
    (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑0 : (a : M ⊗[R] N') → M ⊗[R] Unit) ↔
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
    (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] N') → M ⊗[R] Unit)
Tactic: conv_rhs => rw [← lTensor_exact_iff_exact R M]
-- 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
h : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
N' : Type u_2
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
hf : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N')
    (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
    (⇑(LinearMap.lTensor M LinearMap.id) : (a : M ⊗[R] N') → M ⊗[R] N')
have rw : Function.Injective (α := M ⊗[R] N') (β := M ⊗[R] N') (⇑(LinearMap.lTensor M LinearMap.id) : (a : M ⊗[R] N') → M ⊗[R] N')
Tactic: rw [LinearMap.exact_iff, hf, LinearMap.range_zero, LinearMap.ker_eq_bot]
-- 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
h : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
N' : Type u_2
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
hf : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0
⊢ Function.Injective (α := M ⊗[R] N') (β := M ⊗[R] N')
    (⇑(LinearMap.lTensor M LinearMap.id) : (a : M ⊗[R] N') → M ⊗[R] N')
have hf₁ : Function.Injective.{u_2 + 1, u_2 + 1} (α := N') (β := N') (⇑LinearMap.id : (a : N') → N')
Tactic: apply Module.Flat.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
h : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
N' : Type u_2
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
hf : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0
⊢ f = 0
have this : Function.Exact.{u_1, u_2, u_2} (M := N) (N := N') (P := N') (⇑f : (a : N) → N') (⇑LinearMap.id : (a : N') → N')
Tactic: have := lTensor_reflects_exact R M f LinearMap.id (by
      rw [LinearMap.exact_iff, hf, LinearMap.range_zero, LinearMap.ker_eq_bot]
      apply Module.Flat.lTensor_preserves_injective_linearMap
      exact fun _ _ h => h)
-- 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
h : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
N' : Type u_2
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
hf : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0
this : Function.Exact.{u_1, u_2, u_2} (M := N) (N := N') (P := N') (⇑f : (a : N) → N') (⇑LinearMap.id : (a : N') → N')
⊢ f = 0
have h₁ : ∀ (x : N), Eq.{u_2 + 1} (α := N') ((f : (a : N) → N') x : N') ((0 : (a : N) → N') x : N')
Tactic: ext x
-- 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
h_1 : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
N' : Type u_2
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
h : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0
⊢ Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0
have a : ∀ (n : N) (m : M),
  Eq (α := N' ⊗[R] M)
    (((((AlgebraTensorModule.curry (LinearMap.rTensor M f) : N →ₗ[R] M →ₗ[R] N' ⊗[R] M) : (a : N) → M →ₗ[R] N' ⊗[R] M)
              n :
            M →ₗ[R] N' ⊗[R] M) :
          (a : M) → N' ⊗[R] M)
        m :
      N' ⊗[R] M)
    (((((AlgebraTensorModule.curry 0 : N →ₗ[R] M →ₗ[R] N' ⊗[R] M) : (a : N) → M →ₗ[R] N' ⊗[R] M) n :
            M →ₗ[R] N' ⊗[R] M) :
          (a : M) → N' ⊗[R] M)
        m :
      N' ⊗[R] M)
Tactic: ext n m
-- 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
h_1 : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
N' : Type u_2
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : N →ₗ[R] N'
h : Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0
have a : ∀ (m : M) (n : N),
  Eq (α := M ⊗[R] N')
    (((((AlgebraTensorModule.curry (LinearMap.lTensor M f) : M →ₗ[R] N →ₗ[R] M ⊗[R] N') : (a : M) → N →ₗ[R] M ⊗[R] N')
              m :
            N →ₗ[R] M ⊗[R] N') :
          (a : N) → M ⊗[R] N')
        n :
      M ⊗[R] N')
    (((((AlgebraTensorModule.curry 0 : M →ₗ[R] N →ₗ[R] M ⊗[R] N') : (a : M) → N →ₗ[R] M ⊗[R] N') m :
            N →ₗ[R] M ⊗[R] N') :
          (a : N) → M ⊗[R] N')
        n :
      M ⊗[R] N')
Tactic: ext m n
-- 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
A : Type u_1
inst_3 : Ring A
inst_4 : Algebra R A
inst_5 : FaithfullyFlat R A
m : M
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0 ↔ m = 0
have mp : Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0 → m = 0
Tactic: constructor
-- 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
A : Type u_1
inst_3 : Ring A
inst_4 : Algebra R A
inst_5 : FaithfullyFlat R A
m : M
mp : Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0 → m = 0
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0 ↔ m = 0
have mpr : m = 0 → Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0
Tactic: constructor
-- 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
A : Type u_1
inst_3 : Ring A
inst_4 : Algebra R A
inst_5 : FaithfullyFlat R A
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] 0) 0
have mpr : Eq (α := A ⊗[R] M) 0 0
Tactic: rw [tmul_zero]
-- 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
A : Type u_1
inst_3 : Ring A
inst_4 : Algebra R A
inst_5 : FaithfullyFlat R A
m : M
h : Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0
f : R →ₗ[R] M := (LinearMap.flip (LinearMap.lsmul R M) : (a : M) → R →ₗ[R] M) m
⊢ m = 0
have mp : f = 0
Tactic: suffices f = 0 by simpa [f] using DFunLike.congr_fun this 1
-- 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
A : Type u_1
inst_3 : Ring A
inst_4 : Algebra R A
inst_5 : FaithfullyFlat R A
m : M
h : Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0
f : R →ₗ[R] M := (LinearMap.flip (LinearMap.lsmul R M) : (a : M) → R →ₗ[R] M) m
⊢ f = 0
have mp : Eq (α := A ⊗[R] R →ₗ[R] A ⊗[R] M) (LinearMap.lTensor A f) 0
Tactic: rw [Module.FaithfullyFlat.zero_iff_lTensor_zero R A]
-- 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
A : Type u_1
inst_3 : Ring A
inst_4 : Algebra R A
inst_5 : FaithfullyFlat R A
m : M
h : Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0
f : R →ₗ[R] M := (LinearMap.flip (LinearMap.lsmul R M) : (a : M) → R →ₗ[R] M) m
⊢ Eq (α := A ⊗[R] R →ₗ[R] A ⊗[R] M) (LinearMap.lTensor A f) 0
have mp : ∀ (a : A),
  Eq (α := A ⊗[R] M)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor A f) : A →ₗ[R] R →ₗ[R] A ⊗[R] M) : (a : A) → R →ₗ[R] A ⊗[R] M) a :
          R →ₗ[R] A ⊗[R] M) :
        (a : R) → A ⊗[R] M)
      1)
    (((((AlgebraTensorModule.curry 0 : A →ₗ[R] R →ₗ[R] A ⊗[R] M) : (a : A) → R →ₗ[R] A ⊗[R] M) a : R →ₗ[R] A ⊗[R] M) :
        (a : R) → A ⊗[R] M)
      1)
Tactic: ext a
-- 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
A : Type u_1
inst_3 : Ring A
inst_4 : Algebra R A
inst_5 : FaithfullyFlat R A
m : M
h : Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0
f : R →ₗ[R] M := (LinearMap.flip (LinearMap.lsmul R M) : (a : M) → R →ₗ[R] M) m
a : A
⊢ Eq (α := A ⊗[R] M)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor A f) : A →ₗ[R] R →ₗ[R] A ⊗[R] M) : (a : A) → R →ₗ[R] A ⊗[R] M) a :
          R →ₗ[R] A ⊗[R] M) :
        (a : R) → A ⊗[R] M)
      1)
    (((((AlgebraTensorModule.curry 0 : A →ₗ[R] R →ₗ[R] A ⊗[R] M) : (a : A) → R →ₗ[R] A ⊗[R] M) a : R →ₗ[R] A ⊗[R] M) :
        (a : R) → A ⊗[R] M)
      1)
have h₁ : HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] m) = HSMul.hSMul (β := A ⊗[R] M) a 0
Tactic: apply_fun (a • ·) at h
Cleared hypotheses: h
-- 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
A : Type u_1
inst_3 : Ring A
inst_4 : Algebra R A
inst_5 : FaithfullyFlat R A
m : M
f : R →ₗ[R] M := (LinearMap.flip (LinearMap.lsmul R M) : (a : M) → R →ₗ[R] M) m
a : A
h : HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] m) = HSMul.hSMul (β := A ⊗[R] M) a 0
⊢ Eq (α := A ⊗[R] M)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor A f) : A →ₗ[R] R →ₗ[R] A ⊗[R] M) : (a : A) → R →ₗ[R] A ⊗[R] M) a :
          R →ₗ[R] A ⊗[R] M) :
        (a : R) → A ⊗[R] M)
      1)
    (((((AlgebraTensorModule.curry 0 : A →ₗ[R] R →ₗ[R] A ⊗[R] M) : (a : A) → R →ₗ[R] A ⊗[R] M) a : R →ₗ[R] A ⊗[R] M) :
        (a : R) → A ⊗[R] M)
      1)
have h₁ : Eq (α := A ⊗[R] M) (a ⊗ₜ[R] m) 0
Tactic: rw [smul_zero, smul_tmul', smul_eq_mul, mul_one] at h
Cleared hypotheses: h
-- 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
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (LinearMap.lTensor M LinearMap.id) 0
have a : ∀ (x_2 : M) (x_3 : N),
  Eq (α := M ⊗[R] N)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor M LinearMap.id) : M →ₗ[R] N →ₗ[R] M ⊗[R] N) :
                (a : M) → N →ₗ[R] M ⊗[R] N)
              x_2 :
            N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        x_3 :
      M ⊗[R] N)
    (((((AlgebraTensorModule.curry 0 : M →ₗ[R] N →ₗ[R] M ⊗[R] N) : (a : M) → N →ₗ[R] M ⊗[R] N) x_2 : N →ₗ[R] M ⊗[R] N) :
          (a : N) → M ⊗[R] N)
        x_3 :
      M ⊗[R] N)
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
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (M ⊗[R] N)
⊢ Subsingleton N
have this : Eq (α := N →ₗ[R] N) LinearMap.id 0
Tactic: have := Z (LinearMap.id : N →ₗ[R] N) |>.1 (by ext; exact Subsingleton.elim _ _)
-- 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
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (M ⊗[R] N)
this : Eq (α := N →ₗ[R] N) LinearMap.id 0
⊢ Subsingleton N
have rw : ∀ (y : N), y = 0
Tactic: rw [subsingleton_iff_forall_eq 0]
-- 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
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
⊢ Eq (α := N ⊗[R] M →ₗ[R] N ⊗[R] M) (LinearMap.rTensor M LinearMap.id) 0
have a : ∀ (x_2 : N) (x_3 : M),
  Eq (α := N ⊗[R] M)
    (((((AlgebraTensorModule.curry (LinearMap.rTensor M LinearMap.id) : N →ₗ[R] M →ₗ[R] N ⊗[R] M) :
                (a : N) → M →ₗ[R] N ⊗[R] M)
              x_2 :
            M →ₗ[R] N ⊗[R] M) :
          (a : M) → N ⊗[R] M)
        x_3 :
      N ⊗[R] M)
    (((((AlgebraTensorModule.curry 0 : N →ₗ[R] M →ₗ[R] N ⊗[R] M) : (a : N) → M →ₗ[R] N ⊗[R] M) x_2 : M →ₗ[R] N ⊗[R] M) :
          (a : M) → N ⊗[R] M)
        x_3 :
      N ⊗[R] M)
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
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N
have this : Eq (α := N →ₗ[R] N) LinearMap.id 0
Tactic: have := Z (LinearMap.id : N →ₗ[R] N) |>.1 (by ext; exact Subsingleton.elim _ _)
-- 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
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
this : Eq (α := N →ₗ[R] N) LinearMap.id 0
⊢ Subsingleton N
have rw : ∀ (y : N), y = 0
Tactic: rw [subsingleton_iff_forall_eq 0]
-- 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
⊢ FaithfullyFlat R M
have rw : Flat R M ∧
  ∀ {N : Type (max u_1 u_3)} [inst_9 : AddCommGroup N] [inst_10 : Module R N] {N' : Type (max u_1 u_3)}
    [inst_11 : AddCommGroup N'] [inst_12 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0 ↔ f = 0
Tactic: rw [iff_zero_iff_lTensor_zero]
-- 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
⊢ Flat R M ∧
    ∀ {N : Type (max u_1 u_3)} [inst_9 : AddCommGroup N] [inst_10 : Module R N] {N' : Type (max u_1 u_3)}
      [inst_11 : AddCommGroup N'] [inst_12 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0 ↔ f = 0
have refine : ∀ (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
Tactic: refine ⟨Module.Flat.trans R S M, @fun N _ _ N' _ _ f => ⟨fun aux => ?_, fun eq => eq ▸ by simp⟩⟩