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
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
mem : Membership.mem (γ := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ x
⊢ ∃ (c : TensorProduct.{u, u_3, v} R (↥E) M →₀ R),
    (↑c.support : Set (↥E ⊗[R] M)) ⊆ {t : TensorProduct.{u, u_3, v} R (↥E) M | ∃ (m : ↥E) (n : M), m ⊗ₜ[R] n = t} ∧
      (c.sum fun (mi : TensorProduct.{u, u_3, v} R (↥E) M) (r : R) ↦ r • mi) = x

Tactic:
rw [← TensorProduct.span_tmul_eq_top, Submodule.mem_span_set] at mem

Premises used: TensorProduct.span_tmul_eq_top, Submodule.mem_span_set
-- 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
mem :
  ∃ (c : TensorProduct.{u, u_3, v} R (↥E) M →₀ R),
    (↑c.support : Set (↥E ⊗[R] M)) ⊆ {t : TensorProduct.{u, u_3, v} R (↥E) M | ∃ (m : ↥E) (n : M), m ⊗ₜ[R] n = t} ∧
      (c.sum fun (mi : TensorProduct.{u, u_3, v} R (↥E) M) (r : R) ↦ r • mi) = x
h :
  ∀ (c : TensorProduct.{u, u_3, v} R (↥E) M →₀ R)
    (hc :
      (↑c.support : Set (↥E ⊗[R] M)) ⊆ {t : TensorProduct.{u, u_3, v} R (↥E) M | ∃ (m : ↥E) (n : M), m ⊗ₜ[R] n = t}),
    Eq (α := TensorProduct.{u, u_3, v} R (↥E) M) (c.sum fun (mi : TensorProduct.{u, u_3, v} R (↥E) M) (r : R) ↦ r • mi)
      0
⊢ x = 0

Tactic:
obtain ⟨c, hc, rfl⟩ := mem

Premises used: rfl
-- 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)
c : TensorProduct.{u, u_3, v} R (↥E) M →₀ R
hc : (↑c.support : Set (↥E ⊗[R] M)) ⊆ {t : TensorProduct.{u, u_3, v} R (↥E) M | ∃ (m : ↥E) (n : M), m ⊗ₜ[R] n = t}
h :
  ∀ (b : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → ↥E)
    (a : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → M)
    (hy :
      ∀ ⦃a_1 : TensorProduct.{u, u_3, v} R (↥E) M⦄ (a_2 : a_1 ∈ (↑c.support : Set (↥E ⊗[R] M))),
        b a_2 ⊗ₜ[R] a a_2 = a_1),
    Eq (α := TensorProduct.{u, u_3, v} R (↥E) M) (c.sum fun (mi : TensorProduct.{u, u_3, v} R (↥E) M) (r : R) ↦ r • mi)
      0
⊢ Eq (α := TensorProduct.{u, u_3, v} R (↥E) M) (c.sum fun (mi : TensorProduct.{u, u_3, v} R (↥E) M) (r : R) ↦ r • mi) 0

Tactic:
choose b a hy using hc
-- 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)
c : TensorProduct.{u, u_3, v} R (↥E) M →₀ R
b : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → ↥E
a : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → M
hy : ∀ ⦃a_1 : TensorProduct.{u, u_3, v} R (↥E) M⦄ (a_2 : a_1 ∈ (↑c.support : Set (↥E ⊗[R] M))), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ c.support → R :=
  fun (a : TensorProduct.{u, u_3, v} R (↥E) M) (ha : a ∈ c.support) ↦
    ⋯.choose (p := fun (a_1 : R) ↦
      HSMul.hSMul (β := N3) a_1 ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) = (↑(b ha) : N3))
⊢ ∀ ⦃i : TensorProduct.{u, u_3, v} R (↥E) M⦄ (hi : i ∈ c.support),
    b hi =
      HSMul.hSMul (β := ↥E) (r hi)
        (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ : ↥E)

Tactic:
have hr : ∀ ⦃i : E ⊗[R] M⦄ (hi : i ∈ c.support), b hi =
        r hi • ⟨l23 (l12 n1), Submodule.mem_span_singleton_self _⟩ := fun a ha =>
      Subtype.ext <| Submodule.mem_span_singleton.1 (b ha).2 |>.choose_spec.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
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)
c : TensorProduct.{u, u_3, v} R (↥E) M →₀ R
b : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → ↥E
a : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → M
hy : ∀ ⦃a_1 : TensorProduct.{u, u_3, v} R (↥E) M⦄ (a_2 : a_1 ∈ (↑c.support : Set (↥E ⊗[R] M))), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ c.support → R :=
  fun (a : TensorProduct.{u, u_3, v} R (↥E) M) (ha : a ∈ c.support) ↦
    ⋯.choose (p := fun (a_1 : R) ↦
      HSMul.hSMul (β := N3) a_1 ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) = (↑(b ha) : N3))
hr :
  ∀ ⦃i : TensorProduct.{u, u_3, v} R (↥E) M⦄ (hi : i ∈ c.support),
    b hi =
      HSMul.hSMul (β := ↥E) (r hi)
        (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ : ↥E)
⊢ Eq (α := TensorProduct.{u, u_3, v} R (↥E) M) (c.sum fun (mi : TensorProduct.{u, u_3, v} R (↥E) M) (r : R) ↦ r • mi) 0

Tactic:
Finset.sum_eq_zero fun i hi => show c i • i = 0 from
      (Module.Flat.rTensor_preserves_injective_linearMap (M := M) E.subtype <|
              Submodule.injective_subtype E) ?_

Premises used: Finset.sum_eq_zero, Finsupp.sum, Submodule.injective_subtype, Submodule.subtype, Module.Flat.rTensor_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
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)
c : TensorProduct.{u, u_3, v} R (↥E) M →₀ R
b : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → ↥E
a : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ (↑c.support : Set (↥E ⊗[R] M)) → M
hy : ∀ ⦃a_1 : TensorProduct.{u, u_3, v} R (↥E) M⦄ (a_2 : a_1 ∈ (↑c.support : Set (↥E ⊗[R] M))), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : TensorProduct.{u, u_3, v} R (↥E) M⦄ → a ∈ c.support → R :=
  fun (a : TensorProduct.{u, u_3, v} R (↥E) M) (ha : a ∈ c.support) ↦
    ⋯.choose (p := fun (a_1 : R) ↦
      HSMul.hSMul (β := N3) a_1 ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2) : N3) = (↑(b ha) : N3))
hr :
  ∀ ⦃i : TensorProduct.{u, u_3, v} R (↥E) M⦄ (hi : i ∈ c.support),
    b hi =
      HSMul.hSMul (β := ↥E) (r hi)
        (Subtype.mk (p := fun (x : N3) ↦ x ∈ E) ((l23 : (a : N2) → N3) ((l12 : (a : N1) → N2) n1 : N2)) ⋯ : ↥E)
h :
  ∀ (i : TensorProduct.{u, u_3, v} R (↥E) M) (hi : i ∈ c.support),
    Eq (α := N3 ⊗[R] M)
      ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M)
          (HSMul.hSMul (α := R) ((c : (a : ↥E ⊗[R] M) → R) i : R) i) :
        N3 ⊗[R] M)
      ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0 : N3 ⊗[R] M)
⊢ Eq (α := TensorProduct.{u, u_3, v} R (↥E) M) (c.sum fun (mi : TensorProduct.{u, u_3, v} R (↥E) M) (r : R) ↦ r • mi) 0

Tactic:
refine Finset.sum_eq_zero fun i hi => show c i • i = 0 from
      (Module.Flat.rTensor_preserves_injective_linearMap (M := M) E.subtype <|
              Submodule.injective_subtype E) ?_

Premises used: Finset.sum_eq_zero, Submodule.injective_subtype, Submodule.subtype, Module.Flat.rTensor_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
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)) ⊤ ⊥

Tactic:
have eq0 : (⊤ : Submodule R (E ⊗[R] M)) = ⊥ := by
    -- suppose `x ∈ E ⊗ M`. We will show `x = 0`.
    ext x
    simp only [Submodule.mem_top, Submodule.mem_bot, true_iff]
    have mem : x ∈ (⊤ : Submodule R _) := ⟨⟩
    rw [← TensorProduct.span_tmul_eq_top, Submodule.mem_span_set] at mem
    obtain ⟨c, hc, rfl⟩ := mem
    choose b a hy using hc
    let r : ⦃a : E ⊗[R] M⦄ → a ∈ ↑c.support → R := fun a ha =>
      Submodule.mem_span_singleton.1 (b ha).2 |>.choose
    have hr : ∀ ⦃i : E ⊗[R] M⦄ (hi : i ∈ c.support), b hi =
        r hi • ⟨l23 (l12 n1), Submodule.mem_span_singleton_self _⟩ := fun a ha =>
      Subtype.ext <| Submodule.mem_span_singleton.1 (b ha).2 |>.choose_spec.symm
    -- Since `M` is flat and `E -> N1` is injective, we only need to check that x = 0
    -- in `N1 ⊗ M`. We write `x = ∑ μᵢ • (l23 (l12 n1)) ⊗ mᵢ = ∑ μᵢ • 0 = 0`
    -- (remember `E = span {l23 (l12 n1)}` and `eq1`)
    refine Finset.sum_eq_zero fun i hi => show c i • i = 0 from
      (Module.Flat.rTensor_preserves_injective_linearMap (M := M) E.subtype <|
              Submodule.injective_subtype E) ?_
    rw [← hy hi, hr hi, smul_tmul, map_smul, LinearMap.rTensor_tmul, Submodule.subtype_apply, eq1,
      smul_zero, map_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
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)
eq0 : Eq (α := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ ⊥
⊢ Subsingleton (TensorProduct.{u, u_3, v} R (↥E) M)

Tactic:
have : Subsingleton (E ⊗[R] M) := subsingleton_iff_forall_eq 0 |>.2 fun x =>
    show x ∈ (⊥ : Submodule R _) from eq0 ▸ ⟨⟩
-- 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)
eq0 : Eq (α := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ ⊥
this : Subsingleton (TensorProduct.{u, u_3, v} R (↥E) M)
⊢ False

Tactic:
not_subsingleton_iff_nontrivial.2 inferInstance <| fl.rTensor_reflects_triviality R M E

Premises used: Iff.mpr, Membership.mem, inferInstance, Subtype, not_subsingleton_iff_nontrivial, 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
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)
eq0 : Eq (α := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ ⊥
this : Subsingleton (TensorProduct.{u, u_3, v} R (↥E) M)
⊢ False

Tactic:
exact not_subsingleton_iff_nontrivial.2 inferInstance <| fl.rTensor_reflects_triviality R M E

Premises used: Iff.mpr, Membership.mem, inferInstance, Subtype, not_subsingleton_iff_nontrivial, 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
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)
⊢ l12.range ≤ l23.ker

Tactic:
have complex : LinearMap.range l12 ≤ LinearMap.ker l23 := range_le_ker_of_exact_rTensor R M _ _ ex
-- 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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
triv_coh : Subsingleton H
⊢ l23.ker ≤ l12.range

Tactic:
rw [Submodule.Quotient.subsingleton_iff, Submodule.range_inclusion,
      Submodule.comap_subtype_eq_top] at triv_coh

Premises used: Submodule.comap_subtype_eq_top, Submodule.range_inclusion, Submodule.Quotient.subsingleton_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
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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
triv_coh : l23.ker ≤ l12.range
⊢ l23.ker = l12.range

Tactic:
le_antisymm triv_coh complex

Premises used: le_antisymm
-- 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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
triv_coh : l23.ker ≤ l12.range
⊢ l23.ker = l12.range

Tactic:
exact le_antisymm triv_coh complex

Premises used: le_antisymm
-- 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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
suffices : Subsingleton H
⊢ l23.ker = l12.range

Tactic:
suffices triv_coh : Subsingleton H by
    rw [Submodule.Quotient.subsingleton_iff, Submodule.range_inclusion,
      Submodule.comap_subtype_eq_top] at triv_coh
    exact le_antisymm triv_coh complex
-- 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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
suffices : Subsingleton (H ⊗[R] M)
⊢ Subsingleton H

Tactic:
suffices Subsingleton (H ⊗[R] M) from rTensor_reflects_triviality R M H