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
h : Flat R M
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
simp : ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
⊢ Nontrivial N → Nontrivial (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N

Tactic:
simp only [← not_subsingleton_iff_nontrivial]

Premises used: not_subsingleton_iff_nontrivial
-- 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)
x : AddCommGroup N
x_1 : Module R N
mp : (¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)) → Subsingleton (N ⊗[R] M) → Subsingleton N
mpr : (Subsingleton (N ⊗[R] M) → Subsingleton N) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mp₁ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₂ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₃ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₄ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₅ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₆ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
mpr₁ : ¬Subsingleton (N ⊗[R] M) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mpr₂ : Subsingleton N → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mpr₃ : ¬Subsingleton (N ⊗[R] M) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mpr₄ : Subsingleton N → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mpr₅ : ¬Subsingleton (N ⊗[R] M) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mpr₆ : Subsingleton N → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mp₇ mp₈ mp₉ : Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₁₀ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
mpr₇ : Subsingleton N → ¬Subsingleton N → Subsingleton (N ⊗[R] M) → False
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N

Tactic:
tauto
-- 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 ↔
    Flat R M ∧
      ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (M ⊗[R] N)

Tactic:
iff_flat_and_rTensor_faithful R M |>.trans
  ⟨fun ⟨flat, faithful⟩ => ⟨flat, fun N _ _ _ =>
      letI := faithful N inferInstance; (TensorProduct.comm R M N).toEquiv.nontrivial⟩,
    fun ⟨flat, faithful⟩ => ⟨flat, fun N _ _ _ =>
      letI := faithful N inferInstance; (TensorProduct.comm R M N).symm.toEquiv.nontrivial⟩⟩

Premises used: LinearEquiv.symm, TensorProduct.comm, Equiv.nontrivial, Module.Flat, And, And.intro, Iff.intro, LinearEquiv.toEquiv, Iff.trans, _private.0.Module.FaithfullyFlat.iff_flat_and_lTensor_faithful.match_1, _private.0.Module.FaithfullyFlat.iff_flat_and_rTensor_faithful.match_1, Module.FaithfullyFlat.iff_flat_and_rTensor_faithful
-- 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)
x : AddCommGroup N
x_1 : Module R N
simp : ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
⊢ Nontrivial N → Nontrivial (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N

Tactic:
simp only [← not_subsingleton_iff_nontrivial]

Premises used: not_subsingleton_iff_nontrivial
-- 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)
x : AddCommGroup N
x_1 : Module R N
mp : (¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)) → Subsingleton (M ⊗[R] N) → Subsingleton N
mpr : (Subsingleton (M ⊗[R] N) → Subsingleton N) → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
mp₁ : ¬¬Subsingleton N → Subsingleton (M ⊗[R] N) → Subsingleton N
mp₂ : ¬Subsingleton (M ⊗[R] N) → Subsingleton (M ⊗[R] N) → Subsingleton N
mp₃ : ¬¬Subsingleton N → Subsingleton (M ⊗[R] N) → Subsingleton N
mp₄ : ¬Subsingleton (M ⊗[R] N) → Subsingleton (M ⊗[R] N) → Subsingleton N
mp₅ : ¬¬Subsingleton N → Subsingleton (M ⊗[R] N) → Subsingleton N
mp₆ : ¬Subsingleton (M ⊗[R] N) → Subsingleton (M ⊗[R] N) → Subsingleton N
mpr₁ : ¬Subsingleton (M ⊗[R] N) → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
mpr₂ : Subsingleton N → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
mpr₃ : ¬Subsingleton (M ⊗[R] N) → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
mpr₄ : Subsingleton N → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
mpr₅ : ¬Subsingleton (M ⊗[R] N) → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
mpr₆ : Subsingleton N → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
mp₇ mp₈ mp₉ : Subsingleton N → Subsingleton (M ⊗[R] N) → Subsingleton N
mp₁₀ : ¬Subsingleton (M ⊗[R] N) → Subsingleton (M ⊗[R] N) → Subsingleton N
mpr₇ : Subsingleton N → ¬Subsingleton N → Subsingleton (M ⊗[R] N) → False
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N

Tactic:
tauto
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R M
e : N ≃ₗ[R] M
rw :
  Flat R N ∧
    ∀ (N_1 : Type (max u u_1)) [inst_6 : AddCommGroup N_1] [inst_7 : Module R N_1],
      Nontrivial N_1 → Nontrivial (N ⊗[R] N_1)
⊢ FaithfullyFlat R N

Tactic:
rw [iff_flat_and_lTensor_faithful]

Premises used: Module.FaithfullyFlat.iff_flat_and_lTensor_faithful
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R M
e : N ≃ₗ[R] M
⊢ Flat R N ∧
    ∀ (N_1 : Type (max u u_1)) [inst_6 : AddCommGroup N_1] [inst_7 : Module R N_1],
      Nontrivial N_1 → Nontrivial (N ⊗[R] N_1)

Tactic:
⟨Flat.of_linearEquiv e,
    fun P _ _ hP ↦ (TensorProduct.congr e (LinearEquiv.refl R P)).toEquiv.nontrivial⟩

Premises used: Equiv.nontrivial, TensorProduct.congr, And.intro, LinearEquiv.toEquiv, Module.Flat.of_linearEquiv, LinearEquiv.refl
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R M
e : N ≃ₗ[R] M
⊢ Flat R N ∧
    ∀ (N_1 : Type (max u u_1)) [inst_6 : AddCommGroup N_1] [inst_7 : Module R N_1],
      Nontrivial N_1 → Nontrivial (N ⊗[R] N_1)

Tactic:
exact ⟨Flat.of_linearEquiv e,
    fun P _ _ hP ↦ (TensorProduct.congr e (LinearEquiv.refl R P)).toEquiv.nontrivial⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M_1 : Type v
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
ι : Type u_1
inst_3 : Nonempty ι
M : ι → Type u_2
inst_4 : (i : ι) → AddCommGroup (M i)
inst_5 : (i : ι) → Module.{u, u_2} R (M i)
inst_6 : ∀ (i : ι), FaithfullyFlat.{u, u_2} R (M i)
rw :
  Flat R (⨁ (i : ι), M i) ∧
    ∀ (N : Type (max u u_1 u_2)) [inst_7 : AddCommGroup N] [inst_8 : Module R N],
      Nontrivial N → Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)

Tactic:
rw [iff_flat_and_lTensor_faithful]

Premises used: Module.FaithfullyFlat.iff_flat_and_lTensor_faithful
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M_1 : Type v
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
ι : Type u_1
inst_3 : Nonempty ι
M : ι → Type u_2
inst_4 : (i : ι) → AddCommGroup (M i)
inst_5 : (i : ι) → Module.{u, u_2} R (M i)
inst_6 : ∀ (i : ι), FaithfullyFlat.{u, u_2} R (M i)
⊢ Flat R (⨁ (i : ι), M i) ∧
    ∀ (N : Type (max u u_1 u_2)) [inst_7 : AddCommGroup N] [inst_8 : Module R N],
      Nontrivial N → Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)

Tactic:
⟨inferInstance, fun N _ _ hN ↦ ?_⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M_1 : Type v
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
ι : Type u_1
inst_3 : Nonempty ι
M : ι → Type u_2
inst_4 : (i : ι) → AddCommGroup (M i)
inst_5 : (i : ι) → Module.{u, u_2} R (M i)
inst_6 : ∀ (i : ι), FaithfullyFlat.{u, u_2} R (M i)
refine :
  ∀ (N : Type (max u u_1 u_2)) (x : AddCommGroup N) (x_1 : Module R N) (hN : Nontrivial N),
    Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
⊢ Flat R (⨁ (i : ι), M i) ∧
    ∀ (N : Type (max u u_1 u_2)) [inst_7 : AddCommGroup N] [inst_8 : Module R N],
      Nontrivial N → Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)

Tactic:
refine ⟨inferInstance, fun N _ _ hN ↦ ?_⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M_1 : Type v
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
ι : Type u_1
inst_3 : Nonempty ι
M : ι → Type u_2
inst_4 : (i : ι) → AddCommGroup (M i)
inst_5 : (i : ι) → Module.{u, u_2} R (M i)
inst_6 : ∀ (i : ι), FaithfullyFlat.{u, u_2} R (M i)
N : Type (max u u_1 u_2)
x : AddCommGroup N
x_1 : Module R N
hN : Nontrivial N
obtain : ∀ (i : ι), Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
⊢ Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)

Tactic:
obtain ⟨i⟩ := ‹Nonempty ι›

Premises used: Nonempty
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M_1 : Type v
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
ι : Type u_1
inst_3 : Nonempty ι
M : ι → Type u_2
inst_4 : (i : ι) → AddCommGroup (M i)
inst_5 : (i : ι) → Module.{u, u_2} R (M i)
inst_6 : ∀ (i : ι), FaithfullyFlat.{u, u_2} R (M i)
N : Type (max u u_1 u_2)
x : AddCommGroup N
x_1 : Module R N
hN : Nontrivial N
i : ι
obtain : ∀ (x_2 y : M i ⊗[R] N) (hxy : x_2 ≠ y), Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
⊢ Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)

Tactic:
obtain ⟨x, y, hxy⟩ := Nontrivial.exists_pair_ne (α := M i ⊗[R] N)

Premises used: Nontrivial.exists_pair_ne
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M_1 : Type v
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
ι : Type u_1
inst_3 : Nonempty ι
M : ι → Type u_2
inst_4 : (i : ι) → AddCommGroup (M i)
inst_5 : (i : ι) → Module.{u, u_2} R (M i)
inst_6 : ∀ (i : ι), FaithfullyFlat.{u, u_2} R (M i)
N : Type (max u u_1 u_2)
x_1 : AddCommGroup N
x_2 : Module R N
hN : Nontrivial N
i : ι
x y : M i ⊗[R] N
hxy : x ≠ y
⊢ Nontrivial (⨁ (i : ι), M i ⊗[R] N)

Tactic:
haveI : Nontrivial (⨁ (i : ι), M i ⊗[R] N) :=
    ⟨DirectSum.of _ i x, DirectSum.of _ i y, fun h ↦ hxy (DirectSum.of_injective i h)⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M_1 : Type v
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
ι : Type u_1
inst_3 : Nonempty ι
M : ι → Type u_2
inst_4 : (i : ι) → AddCommGroup (M i)
inst_5 : (i : ι) → Module.{u, u_2} R (M i)
inst_6 : ∀ (i : ι), FaithfullyFlat.{u, u_2} R (M i)
N : Type (max u u_1 u_2)
x_1 : AddCommGroup N
x_2 : Module R N
hN : Nontrivial N
i : ι
x y : M i ⊗[R] N
hxy : x ≠ y
this : Nontrivial (⨁ (i : ι), M i ⊗[R] N)
⊢ Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)

Tactic:
apply (TensorProduct.directSumLeft R R M N).toEquiv.nontrivial

Premises used: Equiv.nontrivial, TensorProduct.directSumLeft, LinearEquiv.toEquiv
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M_1 : Type v
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
ι : Type u_1
inst_3 : Nonempty ι
M : ι → Type u_2
inst_4 : (i : ι) → AddCommGroup (M i)
inst_5 : (i : ι) → Module.{u, u_2} R (M i)
inst_6 : ∀ (i : ι), FaithfullyFlat.{u, u_2} R (M i)
rw rw₁ rw₂ :
  Flat R (⨁ (i : ι), M i) ∧
    ∀ (N : Type (max u u_1 u_2)) [inst_7 : AddCommGroup N] [inst_8 : Module R N],
      Nontrivial N → Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
rw₃ :
  ∀ (N : Type (max u u_1 u_2)) (x : AddCommGroup N) (x_1 : Module R N) (hN : Nontrivial N),
    Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
rw₄ :
  ∀ (N : Type (max u u_1 u_2)) (x : AddCommGroup N) (x_1 : Module R N) (hN : Nontrivial N) (i : ι),
    Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
rw₅ :
  ∀ (N : Type (max u u_1 u_2)) (x : AddCommGroup N) (x_1 : Module R N) (hN : Nontrivial N) (i : ι) (x_2 y : M i ⊗[R] N)
    (hxy : x_2 ≠ y), Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
rw₆ :
  ∀ (N : Type (max u u_1 u_2)) (x : AddCommGroup N) (x_1 : Module R N) (hN : Nontrivial N) (i : ι) (x_2 y : M i ⊗[R] N)
    (hxy : x_2 ≠ y) (this : Nontrivial (⨁ (i : ι), M i ⊗[R] N)), Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)

Tactic:
classical
  rw [iff_flat_and_lTensor_faithful]
  refine ⟨inferInstance, fun N _ _ hN ↦ ?_⟩
  obtain ⟨i⟩ := ‹Nonempty ι›
  obtain ⟨x, y, hxy⟩ := Nontrivial.exists_pair_ne (α := M i ⊗[R] N)
  haveI : Nontrivial (⨁ (i : ι), M i ⊗[R] N) :=
    ⟨DirectSum.of _ i x, DirectSum.of _ i y, fun h ↦ hxy (DirectSum.of_injective i h)⟩
  apply (TensorProduct.directSumLeft R R M N).toEquiv.nontrivial

Premises used: Nonempty, Module.FaithfullyFlat.iff_flat_and_lTensor_faithful
-- 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
ι : Type v
inst_3 : Nonempty ι
⊢ FaithfullyFlat R (ι →₀ R)

Tactic:
of_linearEquiv _ _ (finsuppLEquivDirectSum R R ι)

Premises used: Module.FaithfullyFlat.of_linearEquiv, finsuppLEquivDirectSum
-- 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
ι : Type v
inst_3 : Nonempty ι
⊢ FaithfullyFlat R (ι →₀ R)

Tactic:
exact of_linearEquiv _ _ (finsuppLEquivDirectSum R R ι)

Premises used: Module.FaithfullyFlat.of_linearEquiv, finsuppLEquivDirectSum
-- 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
ι : Type v
inst_3 : Nonempty ι
⊢ FaithfullyFlat R (ι →₀ R)

Tactic:
classical exact of_linearEquiv _ _ (finsuppLEquivDirectSum R R ι)
-- 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
inst_3 : Nontrivial M
inst_4 : Free R M
⊢ FaithfullyFlat R M

Tactic:
of_linearEquiv _ _ (Free.chooseBasis R M).repr

Premises used: Module.FaithfullyFlat.of_linearEquiv, Module.Basis.repr, Module.Free.chooseBasis
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R M
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton N

Tactic:
⟨fun _ ↦ lTensor_reflects_triviality R M N, fun _ ↦ inferInstance⟩

Premises used: Module.FaithfullyFlat.lTensor_reflects_triviality, inferInstance, Iff.intro
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R N
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton M

Tactic:
⟨fun _ ↦ rTensor_reflects_triviality R N M, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, Module.FaithfullyFlat.rTensor_reflects_triviality
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R M
contrapose! : Subsingleton (M ⊗[R] N) ↔ Subsingleton N
⊢ Nontrivial (M ⊗[R] N) ↔ Nontrivial N

Tactic:
contrapose!
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R M
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton N

Tactic:
subsingleton_tensorProduct_iff_right R M

Premises used: Module.FaithfullyFlat.subsingleton_tensorProduct_iff_right
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R M
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton N

Tactic:
exact subsingleton_tensorProduct_iff_right R M

Premises used: Module.FaithfullyFlat.subsingleton_tensorProduct_iff_right
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R N
contrapose! : Subsingleton (M ⊗[R] N) ↔ Subsingleton M
⊢ Nontrivial (M ⊗[R] N) ↔ Nontrivial M

Tactic:
contrapose!
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R N
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton M

Tactic:
subsingleton_tensorProduct_iff_left R M

Premises used: Module.FaithfullyFlat.subsingleton_tensorProduct_iff_left
-- 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
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R N
⊢ Subsingleton (M ⊗[R] N) ↔ Subsingleton M

Tactic:
exact subsingleton_tensorProduct_iff_left R M

Premises used: Module.FaithfullyFlat.subsingleton_tensorProduct_iff_left
-- 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
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 := N1 ⊗[R] M) (N := N2 ⊗[R] M) (P := N3 ⊗[R] M)
    (⇑(LinearMap.rTensor M l12) : (a : N1 ⊗[R] M) → N2 ⊗[R] M)
    (⇑(LinearMap.rTensor M l23) : (a : N2 ⊗[R] M) → N3 ⊗[R] M)
n1 : N1
by_contra! :
  ∀ (hn1 : Ne.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)), False
⊢ Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)

Tactic:
by_contra! hn1
-- 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
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 := N1 ⊗[R] M) (N := N2 ⊗[R] M) (P := N3 ⊗[R] M)
    (⇑(LinearMap.rTensor M l12) : (a : N1 ⊗[R] M) → N2 ⊗[R] M)
    (⇑(LinearMap.rTensor M l23) : (a : N2 ⊗[R] M) → N3 ⊗[R] M)
n1 : N1
hn1 : Ne.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)
E : Submodule R N3 :=
  Submodule.span R (singleton (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3))
⊢ Nontrivial.{u_3} ↥E

Tactic:
have hE : Nontrivial E :=
    ⟨0, ⟨⟨l23 (l12 n1), Submodule.mem_span_singleton_self _⟩, Subtype.coe_ne_coe.1 hn1.symm⟩⟩
-- 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
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 := N1 ⊗[R] M) (N := N2 ⊗[R] M) (P := N3 ⊗[R] M)
    (⇑(LinearMap.rTensor M l12) : (a : N1 ⊗[R] M) → N2 ⊗[R] M)
    (⇑(LinearMap.rTensor M l23) : (a : N2 ⊗[R] M) → N3 ⊗[R] M)
n1 : N1
hn1 : Ne.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)
E : Submodule R N3 :=
  Submodule.span R (singleton (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3))
hE : Nontrivial.{u_3} ↥E
⊢ ∀ (m : M),
    Eq (α := N3 ⊗[R] M) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) ⊗ₜ[R] m : N3 ⊗[R] M) (0 : N3 ⊗[R] M)

Tactic:
have eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0 := fun m ↦
    ex.apply_apply_eq_zero (n1 ⊗ₜ[R] 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
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 := N1 ⊗[R] M) (N := N2 ⊗[R] M) (P := N3 ⊗[R] M)
    (⇑(LinearMap.rTensor M l12) : (a : N1 ⊗[R] M) → N2 ⊗[R] M)
    (⇑(LinearMap.rTensor M l23) : (a : N2 ⊗[R] M) → N3 ⊗[R] M)
n1 : N1
hn1 : Ne.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)
E : Submodule R N3 :=
  Submodule.span R (singleton (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3))
hE : Nontrivial.{u_3} ↥E
eq1 :
  ∀ (m : M),
    Eq (α := N3 ⊗[R] M) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) ⊗ₜ[R] m : N3 ⊗[R] M) (0 : N3 ⊗[R] M)
h :
  ∀ (x : TensorProduct.{u, u_3, v} R (↥E) M),
    Membership.mem (γ := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ x ↔
      Membership.mem (γ := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊥ x
⊢ Eq (α := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ ⊥

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
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 := N1 ⊗[R] M) (N := N2 ⊗[R] M) (P := N3 ⊗[R] M)
    (⇑(LinearMap.rTensor M l12) : (a : N1 ⊗[R] M) → N2 ⊗[R] M)
    (⇑(LinearMap.rTensor M l23) : (a : N2 ⊗[R] M) → N3 ⊗[R] M)
n1 : N1
hn1 : Ne.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)
E : Submodule R N3 :=
  Submodule.span R (singleton (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3))
hE : Nontrivial.{u_3} ↥E
eq1 :
  ∀ (m : M),
    Eq (α := N3 ⊗[R] M) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) ⊗ₜ[R] m : N3 ⊗[R] M) (0 : N3 ⊗[R] M)
x : TensorProduct.{u, u_3, v} R (↥E) M
h : x = 0
⊢ Membership.mem (γ := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ x ↔
    Membership.mem (γ := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊥ x

Tactic:
simp only [Submodule.mem_top, Submodule.mem_bot, true_iff]

Premises used: Submodule.mem_bot, true_iff, Submodule.mem_top
-- 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
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 := N1 ⊗[R] M) (N := N2 ⊗[R] M) (P := N3 ⊗[R] M)
    (⇑(LinearMap.rTensor M l12) : (a : N1 ⊗[R] M) → N2 ⊗[R] M)
    (⇑(LinearMap.rTensor M l23) : (a : N2 ⊗[R] M) → N3 ⊗[R] M)
n1 : N1
hn1 : Ne.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)
E : Submodule R N3 :=
  Submodule.span R (singleton (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3))
hE : Nontrivial.{u_3} ↥E
eq1 :
  ∀ (m : M),
    Eq (α := N3 ⊗[R] M) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) ⊗ₜ[R] m : N3 ⊗[R] M) (0 : N3 ⊗[R] M)
x : TensorProduct.{u, u_3, v} R (↥E) M
⊢ Membership.mem (γ := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ x

Tactic:
have mem : x ∈ (⊤ : Submodule R _) := ⟨⟩