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
⊢ FaithfullyFlat R M ↔
    ∀ {N1 : Type (max u v)} [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type (max u v)}
      [inst_5 : AddCommGroup N2] [inst_6 : Module R N2] {N3 : Type (max u v)} [inst_7 : AddCommGroup N3]
      [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
      Function.Exact (M := N1) (N := N2) (P := N3) (⇑l12 : (a : N1) → N2) (⇑l23 : (a : N2) → N3) ↔
        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)

Tactic:
simp only [iff_exact_iff_rTensor_exact, LinearMap.rTensor_exact_iff_lTensor_exact]

Premises used: Module.FaithfullyFlat.iff_exact_iff_rTensor_exact, LinearMap.rTensor_exact_iff_lTensor_exact
-- 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
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
rw :
  Function.Injective (α := M ⊗[R] N') (β := M ⊗[R] N')
    (⇑(LinearMap.lTensor M LinearMap.id) : (a : M ⊗[R] N') → M ⊗[R] N')
⊢ 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')

Tactic:
rw [LinearMap.exact_iff, hf, LinearMap.range_zero, LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot, LinearMap.range_zero, LinearMap.exact_iff
-- 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
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
hf₁ : Function.Injective.{u_2 + 1, u_2 + 1} (α := N') (β := N') (⇑LinearMap.id : (a : N') → N')
⊢ Function.Injective (α := M ⊗[R] N') (β := M ⊗[R] N')
    (⇑(LinearMap.lTensor M LinearMap.id) : (a : M ⊗[R] N') → M ⊗[R] N')

Tactic:
apply Module.Flat.lTensor_preserves_injective_linearMap

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
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.{u_2 + 1, u_2 + 1} (α := N') (β := N') (⇑LinearMap.id : (a : N') → N')

Tactic:
fun _ _ h => h

Premises used: Function.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
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.{u_2 + 1, u_2 + 1} (α := N') (β := N') (⇑LinearMap.id : (a : N') → N')

Tactic:
exact fun _ _ h => h
-- 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
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.{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)
-- 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
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')
h₁ : ∀ (x : N), Eq.{u_2 + 1} (α := N') ((f : (a : N) → N') x : N') ((0 : (a : N) → N') x : N')
⊢ f = 0

Tactic:
ext x
-- 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
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')
x : N
⊢ Eq.{u_2 + 1} (α := N') ((f : (a : N) → N') x : N') ((0 : (a : N) → N') x : N')

Tactic:
simpa using this (f x)

Premises used: DFunLike.coe
-- 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
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
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)
⊢ Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0

Tactic:
ext n m
-- 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
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
n : N
m : M
⊢ Eq (α := M ⊗[R] N')
    ((TensorProduct.comm R N' M : (a : N' ⊗[R] M) → M ⊗[R] N')
        (((((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) :
      M ⊗[R] N')
    ((TensorProduct.comm R N' M : (a : N' ⊗[R] M) → M ⊗[R] N')
        (((((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) :
      M ⊗[R] N')

Tactic:
simpa using congr($h (m ⊗ₜ n))
-- 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
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
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:
exact (TensorProduct.comm R N' M).injective <|
    (by simpa using congr($h (m ⊗ₜ n)))

Premises used: TensorProduct.comm, LinearEquiv.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
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
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')
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (LinearMap.lTensor M f) 0

Tactic:
ext m n
-- 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
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
m : M
n : N
⊢ Eq (α := N' ⊗[R] M)
    ((TensorProduct.comm R M N' : (a : M ⊗[R] N') → N' ⊗[R] M)
        (((((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) :
      N' ⊗[R] M)
    ((TensorProduct.comm R M N' : (a : M ⊗[R] N') → N' ⊗[R] M)
        (((((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) :
      N' ⊗[R] M)

Tactic:
simpa using congr($h (n ⊗ₜ m))
-- 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
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
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:
exact (TensorProduct.comm R M N').injective <| (by simpa using congr($h (n ⊗ₜ m)))

Premises used: TensorProduct.comm, LinearEquiv.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
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
mpr : m = 0 → Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] m) 0 ↔ m = 0

Tactic:
constructor
-- 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
A : Type u_1
inst_3 : Ring A
inst_4 : Algebra R A
inst_5 : FaithfullyFlat R A
mpr mpr₁ : Eq (α := A ⊗[R] M) 0 0
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] 0) 0

Tactic:
rw [tmul_zero]

Premises used: TensorProduct.tmul_zero
-- 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
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
this : f = 0
⊢ m = 0

Tactic:
simpa [f] using DFunLike.congr_fun this 1

Premises used: DFunLike.congr_fun, OfNat.ofNat
-- 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
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
mp : f = 0
⊢ m = 0

Tactic:
suffices f = 0 by simpa [f] using DFunLike.congr_fun this 1
-- 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
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
mp : Eq (α := A ⊗[R] R →ₗ[R] A ⊗[R] M) (LinearMap.lTensor A f) 0
⊢ f = 0

Tactic:
rw [Module.FaithfullyFlat.zero_iff_lTensor_zero R A]

Premises used: Module.FaithfullyFlat.zero_iff_lTensor_zero
-- 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
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
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)
⊢ Eq (α := A ⊗[R] R →ₗ[R] A ⊗[R] M) (LinearMap.lTensor A f) 0

Tactic:
ext a
-- 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
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
⊢ HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] m) = HSMul.hSMul (β := A ⊗[R] M) a 0

Tactic:
apply_fun (a • ·) at h

Premises used: HSMul.hSMul
-- 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
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) (a ⊗ₜ[R] m) 0

Tactic:
rw [smul_zero, smul_tmul', smul_eq_mul, mul_one] at h

Premises used: smul_zero, TensorProduct.smul_tmul', smul_eq_mul, mul_one
-- 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
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 : Eq (α := A ⊗[R] M) (a ⊗ₜ[R] m) 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)

Tactic:
simpa [f]
-- 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
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)
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)
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (LinearMap.lTensor M LinearMap.id) 0

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
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)
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:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
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)
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:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
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 (α := N →ₗ[R] N) LinearMap.id 0

Tactic:
have := Z (LinearMap.id : N →ₗ[R] N) |>.1 (by ext; exact Subsingleton.elim _ _)
-- 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
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
rw : ∀ (y : N), y = 0
⊢ Subsingleton N

Tactic:
rw [subsingleton_iff_forall_eq 0]

Premises used: subsingleton_iff_forall_eq, OfNat.ofNat
-- 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
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
⊢ ∀ (y : N), y = 0

Tactic:
fun y => congr($this y)

Premises used: congrArg, id, DFunLike.coe
-- 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
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
⊢ ∀ (y : N), y = 0

Tactic:
exact fun y => congr($this y)

Premises used: congrArg, id, DFunLike.coe