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
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
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)
⊢ ∃ (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 ⟨y, rfl⟩ := hy

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)
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 (↥(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)
      (x + y) =
    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:
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 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:
exact ⟨x + y, 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 := 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)
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)
⊢ 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)

Tactic:
ext
-- 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 := 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)
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:
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 := 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)
a :
  ∀ (x : M) (x_1 : N2),
    Eq (α := N3 ⊗[R] M)
      (((((AlgebraTensorModule.curry
                      (LinearMap.rTensor M l23 ∘ₗ (↑(TensorProduct.comm R M N2) : M ⊗[R] N2 →ₗ[R] N2 ⊗[R] M)) :
                    M →ₗ[R] N2 →ₗ[R] N3 ⊗[R] M) :
                  (a : M) → N2 →ₗ[R] N3 ⊗[R] M)
                x :
              N2 →ₗ[R] N3 ⊗[R] M) :
            (a : N2) → N3 ⊗[R] M)
          x_1 :
        N3 ⊗[R] M)
      (((((AlgebraTensorModule.curry
                      ((↑(TensorProduct.comm R M N3) : M ⊗[R] N3 →ₗ[R] N3 ⊗[R] M) ∘ₗ LinearMap.lTensor M l23) :
                    M →ₗ[R] N2 →ₗ[R] N3 ⊗[R] M) :
                  (a : M) → N2 →ₗ[R] N3 ⊗[R] M)
                x :
              N2 →ₗ[R] N3 ⊗[R] M) :
            (a : N2) → N3 ⊗[R] M)
          x_1 :
        N3 ⊗[R] M)
⊢ Eq (α := M ⊗[R] N2 →ₗ[R] N3 ⊗[R] M)
    (LinearMap.rTensor M l23 ∘ₗ (↑(TensorProduct.comm R M N2) : M ⊗[R] N2 →ₗ[R] N2 ⊗[R] M))
    ((↑(TensorProduct.comm R M N3) : M ⊗[R] N3 →ₗ[R] N3 ⊗[R] M) ∘ₗ LinearMap.lTensor M l23)

Tactic:
ext
-- 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 := 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)
x : M
x_1 : N2
⊢ Eq (α := N3 ⊗[R] M)
    (((((AlgebraTensorModule.curry
                    (LinearMap.rTensor M l23 ∘ₗ (↑(TensorProduct.comm R M N2) : M ⊗[R] N2 →ₗ[R] N2 ⊗[R] M)) :
                  M →ₗ[R] N2 →ₗ[R] N3 ⊗[R] M) :
                (a : M) → N2 →ₗ[R] N3 ⊗[R] M)
              x :
            N2 →ₗ[R] N3 ⊗[R] M) :
          (a : N2) → N3 ⊗[R] M)
        x_1 :
      N3 ⊗[R] M)
    (((((AlgebraTensorModule.curry
                    ((↑(TensorProduct.comm R M N3) : M ⊗[R] N3 →ₗ[R] N3 ⊗[R] M) ∘ₗ LinearMap.lTensor M l23) :
                  M →ₗ[R] N2 →ₗ[R] N3 ⊗[R] M) :
                (a : M) → N2 →ₗ[R] N3 ⊗[R] M)
              x :
            N2 →ₗ[R] N3 ⊗[R] M) :
          (a : N2) → N3 ⊗[R] M)
        x_1 :
      N3 ⊗[R] M)

Tactic:
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
inst_9 : FaithfullyFlat R M
⊢ 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) ↔
    Function.Exact.{u_1, u_2, u_3} (M := N1) (N := N2) (P := N3) (⇑l12 : (a : N1) → N2) (⇑l23 : (a : N2) → N3)

Tactic:
⟨fun ex ↦ rTensor_reflects_exact R M l12 l23 ex, fun e ↦ Module.Flat.rTensor_exact _ e⟩

Premises used: Module.FaithfullyFlat.rTensor_reflects_exact, Module.Flat.rTensor_exact, Iff.intro
-- 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
inst_9 : FaithfullyFlat R M
⊢ 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) ↔
    Function.Exact.{u_1, u_2, u_3} (M := N1) (N := N2) (P := N3) (⇑l12 : (a : N1) → N2) (⇑l23 : (a : N2) → N3)

Tactic:
⟨fun ex ↦ lTensor_reflects_exact R M l12 l23 ex, fun e ↦ Module.Flat.lTensor_exact _ e⟩

Premises used: Module.Flat.lTensor_exact, Module.FaithfullyFlat.lTensor_reflects_exact, Iff.intro
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
rw :
  Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N') (⇑0 : (a : M ⊗[R] Unit) → M ⊗[R] N)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Exact.{0, u_4, u_5} (M := Unit) (N := N) (P := N') (⇑0 : (a : Unit) → N) (⇑f : (a : N) → N')
⊢ Function.Injective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Injective.{u_4 + 1, u_5 + 1} (α := N) (β := N') (⇑f : (a : N) → N')

Tactic:
rw [← LinearMap.exact_zero_iff_injective (M ⊗[R] Unit), ← LinearMap.exact_zero_iff_injective Unit]

Premises used: Unit, LinearMap.exact_zero_iff_injective, TensorProduct
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
rw :
  Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N')
    (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] Unit) → M ⊗[R] N) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
| Function.Exact.{0, u_4, u_5} (M := Unit) (N := N) (P := N') (⇑0 : (a : Unit) → N) (⇑f : (a : N) → N')

Tactic:
rw [← lTensor_exact_iff_exact R M]

Premises used: Module.FaithfullyFlat.lTensor_exact_iff_exact
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
conv_rhs :
  Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N') (⇑0 : (a : M ⊗[R] Unit) → M ⊗[R] N)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N')
      (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] Unit) → M ⊗[R] N) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
⊢ Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N') (⇑0 : (a : M ⊗[R] Unit) → M ⊗[R] N)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Exact.{0, u_4, u_5} (M := Unit) (N := N) (P := N') (⇑0 : (a : Unit) → N) (⇑f : (a : N) → N')

Tactic:
conv_rhs => rw [← lTensor_exact_iff_exact R M]

Premises used: Module.FaithfullyFlat.lTensor_exact_iff_exact
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
⊢ Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N') (⇑0 : (a : M ⊗[R] Unit) → M ⊗[R] N)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Exact (M := M ⊗[R] Unit) (N := M ⊗[R] N) (P := M ⊗[R] N')
      (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] Unit) → M ⊗[R] N) (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')

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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
rw :
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑0 : (a : M ⊗[R] N') → M ⊗[R] Unit) ↔
    Function.Exact.{u_4, u_5, 0} (M := N) (N := N') (P := Unit) (⇑f : (a : N) → N') (⇑0 : (a : N') → Unit)
⊢ Function.Surjective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Surjective.{u_4 + 1, u_5 + 1} (α := N) (β := N') (⇑f : (a : N) → N')

Tactic:
rw [← LinearMap.exact_zero_iff_surjective (M ⊗[R] Unit),
    ← LinearMap.exact_zero_iff_surjective Unit]

Premises used: LinearMap.exact_zero_iff_surjective, Unit, TensorProduct
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
rw :
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
    (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] N') → M ⊗[R] Unit)
| Function.Exact.{u_4, u_5, 0} (M := N) (N := N') (P := Unit) (⇑f : (a : N) → N') (⇑0 : (a : N') → Unit)

Tactic:
rw [← lTensor_exact_iff_exact R M]

Premises used: Module.FaithfullyFlat.lTensor_exact_iff_exact
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
conv_rhs :
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑0 : (a : M ⊗[R] N') → M ⊗[R] Unit) ↔
    Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] N') → M ⊗[R] Unit)
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑0 : (a : M ⊗[R] N') → M ⊗[R] Unit) ↔
    Function.Exact.{u_4, u_5, 0} (M := N) (N := N') (P := Unit) (⇑f : (a : N) → N') (⇑0 : (a : N') → Unit)

Tactic:
conv_rhs => rw [← lTensor_exact_iff_exact R M]

Premises used: Module.FaithfullyFlat.lTensor_exact_iff_exact
-- 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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑0 : (a : M ⊗[R] N') → M ⊗[R] Unit) ↔
    Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] Unit)
      (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(LinearMap.lTensor M 0) : (a : M ⊗[R] N') → M ⊗[R] Unit)

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
N : Type u_4
N' : Type u_5
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N'
inst_5 : Module R N
inst_6 : Module R N'
f : N →ₗ[R] N'
inst_7 : FaithfullyFlat R M
⊢ Function.Bijective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(LinearMap.lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') ↔
    Function.Bijective.{u_4 + 1, u_5 + 1} (α := N) (β := N') (⇑f : (a : N) → N')

Tactic:
simp [Function.Bijective]

Premises used: Function.Bijective
-- 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
iff_exact :
  ∀ {N1 : Type (max u v)} [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type (max u v)}
    [inst_5 : AddCommGroup N2] [inst_6 : Module R N2] {N3 : Type (max u v)} [inst_7 : AddCommGroup N3]
    [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact (M := N1) (N := N2) (P := N3) (⇑l12 : (a : N1) → N2) (⇑l23 : (a : N2) → N3) ↔
      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)
N : Type (max u v)
x_1 : AddCommGroup N
x_2 : Module R N
h : Subsingleton (N ⊗[R] M)
y : N
x : N ⊗[R] M
⊢ Eq (α := PUnit.{(max u v) + 1} ⊗[R] M)
      ((LinearMap.rTensor M 0 : (a : N ⊗[R] M) → PUnit.{(max u v) + 1} ⊗[R] M) x : PUnit.{(max u v) + 1} ⊗[R] M)
      (0 : PUnit.{(max u v) + 1} ⊗[R] M) ↔
    Membership.mem (γ := Set (N ⊗[R] M))
      (Set.range (ι := PUnit.{(max u v) + 1} ⊗[R] M)
        (⇑(LinearMap.rTensor M 0) : (a : PUnit.{(max u v) + 1} ⊗[R] M) → N ⊗[R] M))
      x

Tactic:
simpa using Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
iff_exact :
  ∀ {N1 : Type (max u v)} [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type (max u v)}
    [inst_5 : AddCommGroup N2] [inst_6 : Module R N2] {N3 : Type (max u v)} [inst_7 : AddCommGroup N3]
    [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact (M := N1) (N := N2) (P := N3) (⇑l12 : (a : N1) → N2) (⇑l23 : (a : N2) → N3) ↔
      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)
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h : Subsingleton (N ⊗[R] M)
y : N
⊢ y = 0

Tactic:
simpa [eq_comm] using (iff_exact (0 : PUnit →ₗ[R] N) (0 : N →ₗ[R] PUnit) |>.2 fun x => by
        simpa using Subsingleton.elim _ _) y

Premises used: Iff.mpr, eq_comm, OfNat.ofNat