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)
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
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)
⊢ Subsingleton (H ⊗[R] M)

Tactic:
rw [e.toEquiv.subsingleton_congr, Submodule.Quotient.subsingleton_iff,
    LinearMap.range_eq_top]

Premises used: Equiv.subsingleton_congr, LinearMap.range_eq_top, LinearEquiv.toEquiv, 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
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
⊢ 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)
      0)
    0

Tactic:
simp
-- 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
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
⊢ ∃ (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)
      (0 : TensorProduct.{u, u_2, v} R (↥l23.ker) M)

Tactic:
exact ⟨0, by simp⟩
-- 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
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
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)
⊢ ∃ (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)

Tactic:
rcases x with ⟨x, (hx : l23 x = 0)⟩

Premises used: Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
m : M
x : N2
hx : Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) x : N3) (0 : N3)
⊢ Membership.mem (γ := Submodule R (N2 ⊗[R] M)) (LinearMap.ker (LinearMap.rTensor M l23)) (x ⊗ₜ[R] m)

Tactic:
simp [hx]
-- 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
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
m : M
x : N2
hx : Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) x : N3) (0 : N3)
⊢ Membership.mem (γ := Submodule R (N2 ⊗[R] M)) (LinearMap.ker (LinearMap.rTensor M l23)) (x ⊗ₜ[R] m)

Tactic:
have mem : x ⊗ₜ[R] m ∈ LinearMap.ker (l23.rTensor M) := by simp [hx]
-- 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
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
m : M
x : N2
hx : Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) x : N3) (0 : N3)
mem : Membership.mem (γ := Submodule R (N2 ⊗[R] M)) (LinearMap.ker (LinearMap.rTensor M l23)) (x ⊗ₜ[R] m)
⊢ Membership.mem (γ := Submodule R (N2 ⊗[R] M)) (LinearMap.range (LinearMap.rTensor M l12)) (x ⊗ₜ[R] m)

Tactic:
rw [LinearMap.exact_iff.1 ex] at mem

Premises used: Iff.mp, LinearMap.exact_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
m : M
x : N2
hx : Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) x : N3) (0 : N3)
mem : Membership.mem (γ := Submodule R (N2 ⊗[R] M)) (LinearMap.range (LinearMap.rTensor M l12)) (x ⊗ₜ[R] m)
tmul :
  ∀ (y : N1 ⊗[R] M)
    (hy :
      Eq (α := N2 ⊗[R] M) ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
        (x ⊗ₜ[R] m : N2 ⊗[R] 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)
        (Subtype.mk (p := fun (x : N2) ↦ x ∈ l23.ker) x hx ⊗ₜ[R] m : TensorProduct.{u, u_2, v} R (↥l23.ker) 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)
      (Subtype.mk (p := fun (x : N2) ↦ x ∈ l23.ker) x hx ⊗ₜ[R] m : TensorProduct.{u, u_2, v} R (↥l23.ker) M)

Tactic:
obtain ⟨y, hy⟩ := mem
-- 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
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
m : M
x : N2
hx : Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) x : N3) (0 : N3)
y : N1 ⊗[R] M
hy : Eq (α := N2 ⊗[R] M) ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M) (x ⊗ₜ[R] m : N2 ⊗[R] 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)
      (Subtype.mk (p := fun (x : N2) ↦ x ∈ l23.ker) x hx ⊗ₜ[R] m : TensorProduct.{u, u_2, v} R (↥l23.ker) M)

Tactic:
⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
      Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype
      Subtype.val_injective ?_⟩

Premises used: Subtype.val_injective, LinearMap.ker, LinearMap.rangeRestrict, LinearMap.comp, Exists.intro, Submodule.subtype, DFunLike.coe, Module.Flat.rTensor_preserves_injective_linearMap, LinearMap.rTensor
-- 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
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
m : M
x : N2
hx : Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) x : N3) (0 : N3)
y : N1 ⊗[R] M
hy : Eq (α := N2 ⊗[R] M) ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M) (x ⊗ₜ[R] m : N2 ⊗[R] M)
tmul :
  Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M l23.ker.subtype : (a : ↥l23.ker ⊗[R] M) → N2 ⊗[R] M)
        ((TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
            (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
          ((LinearMap.rTensor M ((Submodule.inclusion complex).rangeRestrict ∘ₗ l12.rangeRestrict) :
              (a : N1 ⊗[R] M) → ↥(Submodule.inclusion complex).range ⊗[R] M)
            y)) :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l23.ker.subtype : (a : ↥l23.ker ⊗[R] M) → N2 ⊗[R] M)
        (Subtype.mk (p := fun (x : N2) ↦ x ∈ l23.ker) x hx ⊗ₜ[R] m) :
      N2 ⊗[R] 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)
      (Subtype.mk (p := fun (x : N2) ↦ x ∈ l23.ker) x hx ⊗ₜ[R] m : TensorProduct.{u, u_2, v} R (↥l23.ker) M)

Tactic:
refine ⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
      Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype
      Subtype.val_injective ?_⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
m : M
x : N2
hx : Eq.{u_3 + 1} (α := N3) ((l23 : (a : N2) → N3) x : N3) (0 : N3)
y : N1 ⊗[R] M
hy : Eq (α := N2 ⊗[R] M) ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M) (x ⊗ₜ[R] m : N2 ⊗[R] M)
tmul :
  Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M l23.ker.subtype : (a : ↥l23.ker ⊗[R] M) → N2 ⊗[R] M)
        ((TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
            (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
          ((LinearMap.rTensor M
                (LinearMap.codRestrict (Submodule.inclusion complex).range
                  (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) ⋯) :
              (a : N1 ⊗[R] M) → ↥(Submodule.inclusion complex).range ⊗[R] M)
            y)) :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l12 : (a : N1 ⊗[R] M) → N2 ⊗[R] M) y : N2 ⊗[R] M)
⊢ Eq (α := N2 ⊗[R] M)
    ((LinearMap.rTensor M l23.ker.subtype : (a : ↥l23.ker ⊗[R] M) → N2 ⊗[R] M)
        ((TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
            (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
          ((LinearMap.rTensor M ((Submodule.inclusion complex).rangeRestrict ∘ₗ l12.rangeRestrict) :
              (a : N1 ⊗[R] M) → ↥(Submodule.inclusion complex).range ⊗[R] M)
            y)) :
      N2 ⊗[R] M)
    ((LinearMap.rTensor M l23.ker.subtype : (a : ↥l23.ker ⊗[R] M) → N2 ⊗[R] M)
        (Subtype.mk (p := fun (x : N2) ↦ x ∈ l23.ker) x hx ⊗ₜ[R] m) :
      N2 ⊗[R] M)

Tactic:
simp only [LinearMap.comp_codRestrict, LinearMap.rTensor_tmul, Submodule.coe_subtype, ← hy]

Premises used: LinearMap.rTensor_tmul, LinearMap.comp_codRestrict, Submodule.coe_subtype
-- 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
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 y : TensorProduct.{u, u_2, v} R (↥l23.ker) M
hx :
  ∃ (a : TensorProduct.{u, u_2, v} R (↥(Submodule.inclusion complex).range) M),
    (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
          (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
        a =
      x
hy :
  ∃ (a : TensorProduct.{u, u_2, v} R (↥(Submodule.inclusion complex).range) M),
    (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
          (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
        a =
      y
add :
  ∀ (x : TensorProduct.{u, u_2, v} R (↥(Submodule.inclusion complex).range) M),
    ∃ (a : TensorProduct.{u, u_2, v} R (↥(Submodule.inclusion complex).range) M),
      (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
            (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
          a =
        HAdd.hAdd (α := 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)
              x :
            TensorProduct.{u, u_2, v} R (↥l23.ker) M)
          y
⊢ ∃ (a : TensorProduct.{u, u_2, v} R (↥(Submodule.inclusion complex).range) M),
    (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
          (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
        a =
      x + y

Tactic:
obtain ⟨x, rfl⟩ := hx

Premises used: rfl