awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ x = 0
have mem : Membership.mem (γ := Submodule R (TensorProduct.{u, u_3, v} R (↥E) M)) ⊤ x
Tactic: have mem : x ∈ (⊤ : Submodule R _) := ⟨⟩
-- 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
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
⊢ x = 0
have 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
Tactic: rw [← TensorProduct.span_tmul_eq_top, Submodule.mem_span_set] at mem
Cleared hypotheses: mem
-- 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
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
⊢ x = 0
have 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
Tactic: obtain ⟨c, hc, rfl⟩ := mem
Cleared hypotheses: x, mem
-- 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)
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
have 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
Tactic: choose b a hy using hc
Cleared hypotheses: hc
-- 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
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))
⊢ 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
have 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)) sorry : ↥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
-- 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)
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
have 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)
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) ?_
-- 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)
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)
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)
have h : Eq (α := N3 ⊗[R] M)
  ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M)
      (HSMul.hSMul (α := R) (β := TensorProduct.{u, u_3, v} R (↥E) M) ((c : (a : ↥E ⊗[R] M) → R) (b hi ⊗ₜ[R] a hi) : R)
        (b hi ⊗ₜ[R] a hi)) :
    N3 ⊗[R] M)
  ((LinearMap.rTensor M E.subtype : (a : ↥E ⊗[R] M) → N3 ⊗[R] M) 0 : N3 ⊗[R] M)
Tactic: rw [← hy hi, hr hi, smul_tmul, map_smul, LinearMap.rTensor_tmul, Submodule.subtype_apply, eq1,
      smul_zero, map_zero]
-- 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
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)
⊢ False
have eq0 : 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]
-- 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
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)) ⊤ ⊥
⊢ False
have this : 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 ▸ ⟨⟩
-- 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)
⊢ l23.ker = l12.range
have complex : l12.range ≤ l23.ker
Tactic: have complex : LinearMap.range l12 ≤ LinearMap.ker l23 := range_le_ker_of_exact_rTensor R M _ _ ex
-- 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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
triv_coh : Subsingleton H
⊢ l23.ker = l12.range
have triv_coh₁ : l23.ker ≤ l12.range
Tactic: rw [Submodule.Quotient.subsingleton_iff, Submodule.range_inclusion,
      Submodule.comap_subtype_eq_top] at triv_coh
Cleared hypotheses: triv_coh
-- 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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
⊢ l23.ker = l12.range
have suffices : Subsingleton H
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
-- 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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
⊢ Subsingleton H
have suffices : Subsingleton (H ⊗[R] M)
Tactic: suffices Subsingleton (H ⊗[R] M) from rTensor_reflects_triviality R M H
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
e : H ⊗[R] M ≃ₗ[R]
  HasQuotient.Quotient (TensorProduct.{u, u_2, v} R (↥l23.ker) M) (B :=
    Submodule R (TensorProduct.{u, u_2, v} R (↥l23.ker) M))
    (LinearMap.range (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id)) :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
⊢ Subsingleton (H ⊗[R] M)
have rw : Function.Surjective (α := TensorProduct.{u, u_2, v} R (↥(Submodule.inclusion complex).range) M) (β :=
  TensorProduct.{u, u_2, v} R (↥l23.ker) M)
  (⇑(TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) :
    (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
Tactic: rw [e.toEquiv.subsingleton_congr, Submodule.Quotient.subsingleton_iff,
    LinearMap.range_eq_top]
-- 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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  HasQuotient.Quotient (TensorProduct.{u, u_2, v} R (↥l23.ker) M) (B :=
    Submodule R (TensorProduct.{u, u_2, v} R (↥l23.ker) M))
    (LinearMap.range (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id)) :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
x : ↥l23.ker
m : M
⊢ ∃ (a : TensorProduct.{u, u_2, v} R (↥(Submodule.inclusion complex).range) M),
    Eq (α := TensorProduct.{u, u_2, v} R (↥l23.ker) M)
      ((TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
            (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
          a :
        TensorProduct.{u, u_2, v} R (↥l23.ker) M)
      (x ⊗ₜ[R] m : TensorProduct.{u, u_2, v} R (↥l23.ker) M)
have tmul : ∀ (x : N2) (hx : Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) x : N3) (0 : N3)),
  ∃ (a : TensorProduct.{u, u_2, v} R (↥(Submodule.inclusion complex).range) M),
    Eq (α := TensorProduct.{u, u_2, v} R (↥l23.ker) M)
      ((TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
            (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
          a :
        TensorProduct.{u, u_2, v} R (↥l23.ker) M)
      (Subtype.mk (p := fun (x : N2) ↦ x ∈ l23.ker) x hx ⊗ₜ[R] m : TensorProduct.{u, u_2, v} R (↥l23.ker) M)
Tactic: rcases x with ⟨x, (hx : l23 x = 0)⟩
Cleared hypotheses: x