-- Mathlib/RingTheory/Flat/EquationalCriterion.lean
theorem tfae_equational_criterion : List.TFAE [
    Flat R M,
    ∀ I : Ideal R, Function.Injective (rTensor M I.subtype),
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ x i = (0 : R ⊗[R] M) →
      VanishesTrivially R f x,
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x,
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 →
      ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] (Fin k →₀ R)) (y : (Fin k →₀ R) →ₗ[R] M),
        x = y ∘ₗ a ∧ a f = 0]

Proof state:
case h.left
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⇑f
x' : Fin l → M := fun i => x (Finsupp.single i 1)
this : ∑ i : Fin l, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j : Fin k, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i : Fin l, f' i * a' i j = 0
⊢ x = linearCombination R y' ∘ₗ linearCombination R fun i => equivFunOnFinite.symm (a' i)

Tactic:
apply Finsupp.basisSingleOne.ext

Result:
case h.left
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⇑f
x' : Fin l → M := fun i => x (Finsupp.single i 1)
this : ∑ i : Fin l, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j : Fin k, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i : Fin l, f' i * a' i j = 0
⊢ ∀ (i : Fin l),
    x (Finsupp.basisSingleOne i) =
      (linearCombination R y' ∘ₗ linearCombination R fun i => equivFunOnFinite.symm (a' i)) (Finsupp.basisSingleOne i)

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⇑f
x' : Fin l → M := fun i => x (Finsupp.single i 1)
this : ∑ i : Fin l, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j : Fin k, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i : Fin l, f' i * a' i j = 0
⊢ ∃ a y, x = y ∘ₗ a ∧ a f = 0

Tactic:
use Finsupp.linearCombination R (fun i ↦ equivFunOnFinite.symm (a' i))

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⇑f
x' : Fin l → M := fun i => x (Finsupp.single i 1)
this : ∑ i : Fin l, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j : Fin k, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i : Fin l, f' i * a' i j = 0
⊢ ∃ y,
    (x = y ∘ₗ linearCombination R fun i => equivFunOnFinite.symm (a' i)) ∧
      (linearCombination R fun i => equivFunOnFinite.symm (a' i)) f = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i : Fin l, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
⊢ IsTrivialRelation f x

Tactic:
let x' : (Fin l →₀ R) →ₗ[R] M := Finsupp.linearCombination R x

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i : Fin l, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
⊢ IsTrivialRelation f x