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)
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)
⊢ ∃ (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)
have mem : 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]
-- 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
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)
⊢ ∃ (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)
have mem₁ : 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
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)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨y, hy⟩ := 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)
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)
have 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)
Tactic: refine ⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
      Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype
      Subtype.val_injective ?_⟩
-- 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
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)
⊢ 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)
have 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) sorry) :
            (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)
Tactic: simp only [LinearMap.comp_codRestrict, LinearMap.rTensor_tmul, Submodule.coe_subtype, ← hy]
-- 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
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)
⊢ 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)
have tmul : Eq (α := N2 ⊗[R] M)
  ((LinearMap.rTensor M l23.ker.subtype ∘ₗ TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
        (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → N2 ⊗[R] M)
      ((LinearMap.rTensor M
            (LinearMap.codRestrict (Submodule.inclusion complex).range
              (Submodule.inclusion complex ∘ₗ l12.rangeRestrict) sorry) :
          (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)
Tactic: rw [← LinearMap.comp_apply, ← LinearMap.rTensor_def, ← LinearMap.rTensor_comp,
      ← LinearMap.comp_apply, ← LinearMap.rTensor_comp, LinearMap.comp_assoc,
      LinearMap.subtype_comp_codRestrict, ← LinearMap.comp_assoc, Submodule.subtype_comp_inclusion,
      LinearMap.subtype_comp_codRestrict]
-- 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 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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, rfl⟩ := hx
Cleared hypotheses: x, hx
-- 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
y : TensorProduct.{u, u_2, v} R (↥l23.ker) M
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
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
have add : ∀ (y : 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.{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)
        ((TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id :
              (a : ↥(Submodule.inclusion complex).range ⊗[R] M) → ↥l23.ker ⊗[R] M)
            y :
          TensorProduct.{u, u_2, v} R (↥l23.ker) M)
Tactic: obtain ⟨y, rfl⟩ := hy
Cleared hypotheses: y, hy
-- 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 : TensorProduct.{u, u_2, v} R (↥l23.ker) 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 =
      x
have zero : ∃ (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: induction x using TensorProduct.induction_on with
  | zero => exact ⟨0, by simp⟩
  -- let `x ⊗ m` be an element in `ker l23 ⊗ M`, then `x ⊗ m` is in the kernel of `l23 ⊗ 𝟙M`.
  -- Since `N1 ⊗ M -l12 ⊗ M-> N2 ⊗ M -l23 ⊗ M-> N3 ⊗ M` is exact, we have that `x ⊗ m` is in
  -- the range of `l12 ⊗ 𝟙M`, i.e. `x ⊗ m = (l12 ⊗ 𝟙M) y` for some `y ∈ N1 ⊗ M` as elements of
  -- `N2 ⊗ M`. We need to prove that `x ⊗ m = (l12 ⊗ 𝟙M) y` still holds in `(ker l23) ⊗ M`.
  -- This is okay because `M` is flat and `ker l23 -> N2` is injective.
  | tmul x m =>
    rcases x with ⟨x, (hx : l23 x = 0)⟩
    have mem : x ⊗ₜ[R] m ∈ LinearMap.ker (l23.rTensor M) := by simp [hx]
    rw [LinearMap.exact_iff.1 ex] at mem
    obtain ⟨y, hy⟩ := mem
    refine ⟨LinearMap.rTensor M (LinearMap.rangeRestrict _ ∘ₗ LinearMap.rangeRestrict l12) y,
      Module.Flat.rTensor_preserves_injective_linearMap (LinearMap.ker l23).subtype
      Subtype.val_injective ?_⟩
    simp only [LinearMap.comp_codRestrict, LinearMap.rTensor_tmul, Submodule.coe_subtype, ← hy]
    rw [← LinearMap.comp_apply, ← LinearMap.rTensor_def, ← LinearMap.rTensor_comp,
      ← LinearMap.comp_apply, ← LinearMap.rTensor_comp, LinearMap.comp_assoc,
      LinearMap.subtype_comp_codRestrict, ← LinearMap.comp_assoc, Submodule.subtype_comp_inclusion,
      LinearMap.subtype_comp_codRestrict]
  | add x y hx hy =>
    obtain ⟨x, rfl⟩ := hx; obtain ⟨y, rfl⟩ := hy
    exact ⟨x + y, by simp⟩
Cleared hypotheses: 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 := M ⊗[R] N1) (N := M ⊗[R] N2) (P := M ⊗[R] N3)
    (⇑(LinearMap.lTensor M l12) : (a : M ⊗[R] N1) → M ⊗[R] N2)
    (⇑(LinearMap.lTensor M l23) : (a : M ⊗[R] N2) → M ⊗[R] N3)
⊢ Eq (α := M ⊗[R] N1 →ₗ[R] N2 ⊗[R] M)
    (LinearMap.rTensor M l12 ∘ₗ (↑(TensorProduct.comm R M N1) : M ⊗[R] N1 →ₗ[R] N1 ⊗[R] M))
    ((↑(TensorProduct.comm R M N2) : M ⊗[R] N2 →ₗ[R] N2 ⊗[R] M) ∘ₗ LinearMap.lTensor M l12)
have a : ∀ (x : M) (x_1 : N1),
  Eq (α := N2 ⊗[R] M)
    (((((AlgebraTensorModule.curry
                    (LinearMap.rTensor M l12 ∘ₗ (↑(TensorProduct.comm R M N1) : M ⊗[R] N1 →ₗ[R] N1 ⊗[R] M)) :
                  M →ₗ[R] N1 →ₗ[R] N2 ⊗[R] M) :
                (a : M) → N1 →ₗ[R] N2 ⊗[R] M)
              x :
            N1 →ₗ[R] N2 ⊗[R] M) :
          (a : N1) → N2 ⊗[R] M)
        x_1 :
      N2 ⊗[R] M)
    (((((AlgebraTensorModule.curry
                    ((↑(TensorProduct.comm R M N2) : M ⊗[R] N2 →ₗ[R] N2 ⊗[R] M) ∘ₗ LinearMap.lTensor M l12) :
                  M →ₗ[R] N1 →ₗ[R] N2 ⊗[R] M) :
                (a : M) → N1 →ₗ[R] N2 ⊗[R] M)
              x :
            N1 →ₗ[R] N2 ⊗[R] M) :
          (a : N1) → N2 ⊗[R] M)
        x_1 :
      N2 ⊗[R] M)
Tactic: ext