-- Mathlib/RingTheory/Flat/Basic.lean
theorem iff_rTensor_exact' [Small.{v'} R] : Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N'']
      [Module R N] [Module R N'] [Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
        Function.Exact f g → Function.Exact (f.rTensor M) (g.rTensor M)

Proof state:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Function.Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ 0 = x

Tactic:
exact (f.map_eq_zero_iff hf).trans eq_comm

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝³ : AddCommGroup N'
x✝² : AddCommGroup N''
x✝¹ : Module R N'
x✝ : Module R N''
f : N' →ₗ[R] N''
hf : Function.Injective ⇑f
x : N' ⊗[R] M
hx : (rTensor M f) x = 0
⊢ x ∈ ⊥

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

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Function.Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ x ∈ Set.range ⇑0

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

Result:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Function.Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ 0 = x

Proof state:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
      [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)

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) ↦ ?_⟩

Result:
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝³ : AddCommGroup N'
x✝² : AddCommGroup N''
x✝¹ : Module R N'
x✝ : Module R N''
f : N' →ₗ[R] N''
hf : Function.Injective ⇑f
x : N' ⊗[R] M
hx : (rTensor M f) x = 0
⊢ x ∈ ⊥