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
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)
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
have mp₇ : Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
Tactic: tauto
-- 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)
x : AddCommGroup N
x_1 : Module R N
⊢ Nontrivial N → Nontrivial (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
have simp : ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
Tactic: simp only [← not_subsingleton_iff_nontrivial]
-- 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)
x : AddCommGroup N
x_1 : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
have mp : (¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)) → Subsingleton (M ⊗[R] N) → Subsingleton N
Tactic: tauto
-- 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)
x : AddCommGroup N
x_1 : Module R N
mp : (¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)) → Subsingleton (M ⊗[R] N) → Subsingleton N
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
have mpr : (Subsingleton (M ⊗[R] N) → Subsingleton N) → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
Tactic: tauto
-- 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)
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)
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
have mp₁ : ¬¬Subsingleton N → Subsingleton (M ⊗[R] N) → Subsingleton N
Tactic: tauto
-- 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)
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
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
have mp₂ : ¬Subsingleton (M ⊗[R] N) → Subsingleton (M ⊗[R] N) → Subsingleton N
Tactic: tauto
-- 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)
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
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
have mpr₁ : ¬Subsingleton (M ⊗[R] N) → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
Tactic: tauto
-- 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)
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)
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
have mpr₂ : Subsingleton N → ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N)
Tactic: tauto
-- 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)
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)
⊢ ¬Subsingleton N → ¬Subsingleton (M ⊗[R] N) ↔ Subsingleton (M ⊗[R] N) → Subsingleton N
have mp₇ : Subsingleton N → Subsingleton (M ⊗[R] N) → Subsingleton N
Tactic: tauto
-- 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_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R M
e : N ≃ₗ[R] M
⊢ FaithfullyFlat R N
have 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)
Tactic: rw [iff_flat_and_lTensor_faithful]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)
have 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)
Tactic: rw [iff_flat_and_lTensor_faithful]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
have 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)
Tactic: refine ⟨inferInstance, fun N _ _ hN ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
⊢ Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
have obtain : ∀ (i : ι), Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
Tactic: obtain ⟨i⟩ := ‹Nonempty ι›
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 : ι
⊢ Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
have obtain : ∀ (x_2 y : M i ⊗[R] N) (hxy : x_2 ≠ y), Nontrivial ((⨁ (i : ι), M i) ⊗[R] N)
Tactic: obtain ⟨x, y, hxy⟩ := Nontrivial.exists_pair_ne (α := M i ⊗[R] N)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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)
have this : 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)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ FaithfullyFlat R (⨁ (i : ι), M i)
have 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)
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
-- 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_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R M
⊢ Nontrivial (M ⊗[R] N) ↔ Nontrivial N
have contrapose! : Subsingleton (M ⊗[R] N) ↔ Subsingleton N
Tactic: contrapose!
-- 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_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : FaithfullyFlat R N
⊢ Nontrivial (M ⊗[R] N) ↔ Nontrivial M
have contrapose! : Subsingleton (M ⊗[R] N) ↔ Subsingleton M
Tactic: contrapose!
-- 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 := 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
⊢ Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)
have by_contra! : ∀ (hn1 : Ne.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) (0 : N3)), False
Tactic: by_contra! hn1
-- 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
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))
⊢ False
have hE : 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⟩⟩
-- 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
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
⊢ False
have 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)
Tactic: have eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0 := fun m ↦
    ex.apply_apply_eq_zero (n1 ⊗ₜ[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
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)
⊢ Eq (α := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ ⊥
have 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
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
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 ↔
    Membership.mem (γ := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊥ x
have h : x = 0
Tactic: simp only [Submodule.mem_top, Submodule.mem_bot, true_iff]