awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
exact1 :
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := TensorProduct.{u, v, u_2} R M (N' ⧸ f.range))
    (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] (N' ⧸ f.range))
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
    (⇑(lTensor M ι ∘ₗ lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] N'')

Tactic:
exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)

Premises used: Module.Flat.lTensor_preserves_injective_linearMap, map_zero, Function.Exact.comp_injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
suffices :
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := TensorProduct.{u, v, u_2} R M (N' ⧸ f.range))
    (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] (N' ⧸ f.range))
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
    (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')

Tactic:
suffices exact1 : Function.Exact (f.lTensor M) (π.lTensor M) by
    rw [show g = ι.comp π from rfl, lTensor_comp]
    exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
x : N'
⊢ Eq (α := N' ⧸ f.range) ((π : (a : N') → N' ⧸ f.range) x : N' ⧸ f.range) (0 : N' ⧸ f.range) ↔
    Membership.mem (γ := Set N') (Set.range.{u_2, u_1 + 1} (ι := N) (⇑f : (a : N) → N')) x

Tactic:
simp [π]
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := TensorProduct.{u, v, u_2} R M (N' ⧸ f.range))
    (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] (N' ⧸ f.range))

Tactic:
exact _root_.lTensor_exact _ (fun x ↦ by simp [π]) Quotient.mk''_surjective

Premises used: lTensor_exact
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
exact1 :
  Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := TensorProduct.{u, u_2, v} R (N' ⧸ f.range) M)
    (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M) (⇑(rTensor M π) : (a : N' ⊗[R] M) → (N' ⧸ f.range) ⊗[R] M)
rw :
  Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
    (⇑(rTensor M ι ∘ₗ rTensor M π) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
⊢ Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
    (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)

Tactic:
rw [show g = ι.comp π from rfl, rTensor_comp]

Premises used: LinearMap.rTensor_comp, rfl
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
exact1 :
  Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := TensorProduct.{u, u_2, v} R (N' ⧸ f.range) M)
    (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M) (⇑(rTensor M π) : (a : N' ⊗[R] M) → (N' ⧸ f.range) ⊗[R] M)
⊢ Injective.{u_2 + 1, u_3 + 1} (α := N' ⧸ f.range) (β := N'') (⇑ι : (a : N' ⧸ f.range) → N'')

Tactic:
simpa [ι, -Subtype.val_injective] using Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
exact1 :
  Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := TensorProduct.{u, u_2, v} R (N' ⧸ f.range) M)
    (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M) (⇑(rTensor M π) : (a : N' ⊗[R] M) → (N' ⧸ f.range) ⊗[R] M)
⊢ Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
    (⇑(rTensor M ι ∘ₗ rTensor M π) : (a : N' ⊗[R] M) → N'' ⊗[R] M)

Tactic:
exact exact1.comp_injective _ (rTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)

Premises used: map_zero, Function.Exact.comp_injective, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
suffices :
  Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := TensorProduct.{u, u_2, v} R (N' ⧸ f.range) M)
    (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M) (⇑(rTensor M π) : (a : N' ⊗[R] M) → (N' ⧸ f.range) ⊗[R] M)
⊢ Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
    (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)

Tactic:
suffices exact1 : Function.Exact (f.rTensor M) (π.rTensor M) by
    rw [show g = ι.comp π from rfl, rTensor_comp]
    exact exact1.comp_injective _ (rTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
⊢ Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := TensorProduct.{u, u_2, v} R (N' ⧸ f.range) M)
    (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M) (⇑(rTensor M π) : (a : N' ⊗[R] M) → (N' ⧸ f.range) ⊗[R] M)

Tactic:
exact _root_.rTensor_exact M (fun x ↦ by simp [π]) Quotient.mk''_surjective

Premises used: rTensor_exact
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
          (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')

Tactic:
⟨fun _ ↦ lTensor_exact _, fun H ↦ iff_lTensor_preserves_injective_linearMap'.mpr
    fun N' N'' _ _ _ _ L hL ↦ LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr
      fun x (hx : _ = 0) ↦ ?_⟩

Premises used: Iff.mpr, Module.Flat.lTensor_exact, LinearMap.ker_eq_bot, Module.Flat.iff_lTensor_preserves_injective_linearMap', Iff.intro, Iff.mp, eq_bot_iff
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
refine :
  ∀
    (H :
      ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
        [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
        Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
          Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'')
            (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N''))
    (N' N'' : Type v') (x : AddCommGroup N') (x_1 : AddCommGroup N'') (x_2 : Module R N') (x_3 : Module R N'')
    (L : N' →ₗ[R] N'') (hL : Injective (α := N') (β := N'') (⇑L : (a : N') → N'')) (x_4 : M ⊗[R] N')
    (hx : Eq (α := M ⊗[R] N'') ((lTensor M L : (a : M ⊗[R] N') → M ⊗[R] N'') x_4 : M ⊗[R] N'') (0 : M ⊗[R] N'')),
    Membership.mem (γ := Submodule R (M ⊗[R] N')) ⊥ x_4
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
          (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')

Tactic:
refine ⟨fun _ ↦ lTensor_exact _, fun H ↦ iff_lTensor_preserves_injective_linearMap'.mpr
    fun N' N'' _ _ _ _ L hL ↦ LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr
      fun x (hx : _ = 0) ↦ ?_⟩
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
    [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
        (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
L : N' →ₗ[R] N''
hL : Injective (α := N') (β := N'') (⇑L : (a : N') → N'')
x_5 : M ⊗[R] N'
hx : Eq (α := M ⊗[R] N'') ((lTensor M L : (a : M ⊗[R] N') → M ⊗[R] N'') x_5 : M ⊗[R] N'') (0 : M ⊗[R] N'')
x : N'
simp_rw : Eq (α := N'') ((L : (a : N') → N'') x : N'') (0 : N'') ↔ 0 = x
⊢ Eq (α := N'') ((L : (a : N') → N'') x : N'') (0 : N'') ↔
    Membership.mem (γ := Set N') (Set.range (ι := PUnit.{v' + 1}) (⇑0 : (a : PUnit.{v' + 1}) → N')) x

Tactic:
simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]

Premises used: LinearMap.zero_apply, Set.mem_range, exists_const
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
    [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
        (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
L : N' →ₗ[R] N''
hL : Injective (α := N') (β := N'') (⇑L : (a : N') → N'')
x_5 : M ⊗[R] N'
hx : Eq (α := M ⊗[R] N'') ((lTensor M L : (a : M ⊗[R] N') → M ⊗[R] N'') x_5 : M ⊗[R] N'') (0 : M ⊗[R] N'')
x : N'
⊢ Eq (α := N'') ((L : (a : N') → N'') x : N'') (0 : N'') ↔ 0 = x

Tactic:
(L.map_eq_zero_iff hL).trans eq_comm

Premises used: eq_comm, Iff.trans, LinearMap.map_eq_zero_iff
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
    [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
        (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
L : N' →ₗ[R] N''
hL : Injective (α := N') (β := N'') (⇑L : (a : N') → N'')
x_5 : M ⊗[R] N'
hx : Eq (α := M ⊗[R] N'') ((lTensor M L : (a : M ⊗[R] N') → M ⊗[R] N'') x_5 : M ⊗[R] N'') (0 : M ⊗[R] N'')
x : N'
⊢ Eq (α := N'') ((L : (a : N') → N'') x : N'') (0 : N'') ↔ 0 = x

Tactic:
exact (L.map_eq_zero_iff hL).trans eq_comm

Premises used: eq_comm, Iff.trans, LinearMap.map_eq_zero_iff
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
    [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
        (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
L : N' →ₗ[R] N''
hL : Injective (α := N') (β := N'') (⇑L : (a : N') → N'')
x : M ⊗[R] N'
hx : Eq (α := M ⊗[R] N'') ((lTensor M L : (a : M ⊗[R] N') → M ⊗[R] N'') x : M ⊗[R] N'') (0 : M ⊗[R] N'')
⊢ Membership.mem (γ := Submodule R (M ⊗[R] N')) ⊥ x

Tactic:
simpa [Eq.comm] using @H PUnit N' N'' _ _ _ _ _ _ 0 L (fun x ↦ by
    simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]
    exact (L.map_eq_zero_iff hL).trans eq_comm) x |>.mp hx

Premises used: Iff.mp, Eq.comm
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type (max u v)⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : AddCommGroup N'']
      [inst_6 : Module R N] [inst_7 : Module R N'] [inst_8 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
          (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')

Tactic:
iff_lTensor_exact'

Premises used: Module.Flat.iff_lTensor_exact'
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
          (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)

Tactic:
⟨fun _ ↦ rTensor_exact _, fun H ↦ iff_rTensor_preserves_injective_linearMap'.mpr
    fun N' N'' _ _ _ _ f hf ↦ LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr
      fun x (hx : _ = 0) ↦ ?_⟩

Premises used: Iff.mpr, LinearMap.ker_eq_bot, Module.Flat.rTensor_exact, Iff.intro, Iff.mp, eq_bot_iff, Module.Flat.iff_rTensor_preserves_injective_linearMap'
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
refine :
  ∀
    (H :
      ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
        [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
        Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
          Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M)
            (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M) (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M))
    (N' N'' : Type v') (x : AddCommGroup N') (x_1 : AddCommGroup N'') (x_2 : Module R N') (x_3 : Module R N'')
    (f : N' →ₗ[R] N'') (hf : Injective (α := N') (β := N'') (⇑f : (a : N') → N'')) (x_4 : N' ⊗[R] M)
    (hx : Eq (α := N'' ⊗[R] M) ((rTensor M f : (a : N' ⊗[R] M) → N'' ⊗[R] M) x_4 : N'' ⊗[R] M) (0 : N'' ⊗[R] M)),
    Membership.mem (γ := Submodule R (N' ⊗[R] M)) ⊥ x_4
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
          (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)

Tactic:
refine ⟨fun _ ↦ rTensor_exact _, fun H ↦ iff_rTensor_preserves_injective_linearMap'.mpr
    fun N' N'' _ _ _ _ f hf ↦ LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr
      fun x (hx : _ = 0) ↦ ?_⟩
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
    [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
        (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
f : N' →ₗ[R] N''
hf : Injective (α := N') (β := N'') (⇑f : (a : N') → N'')
x_5 : N' ⊗[R] M
hx : Eq (α := N'' ⊗[R] M) ((rTensor M f : (a : N' ⊗[R] M) → N'' ⊗[R] M) x_5 : N'' ⊗[R] M) (0 : N'' ⊗[R] M)
x : N'
simp_rw : Eq (α := N'') ((f : (a : N') → N'') x : N'') (0 : N'') ↔ 0 = x
⊢ Eq (α := N'') ((f : (a : N') → N'') x : N'') (0 : N'') ↔
    Membership.mem (γ := Set N') (Set.range (ι := PUnit.{v' + 1}) (⇑0 : (a : PUnit.{v' + 1}) → N')) x

Tactic:
simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]

Premises used: LinearMap.zero_apply, Set.mem_range, exists_const