-- Lean 4 proof step from Mathlib.RingTheory.Flat.EquationalCriterion (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
tfae_have tfae_have₁ tfae_have₂ :
  ∀
    (tfae_1_iff_2 :
      Flat R M ↔
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M)),
    [Flat R M,
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M),
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x,
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x,
        ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
          Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M) →
            ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
              x = y ∘ₗ a ∧
                Eq (α := Fin k →₀ R) ((a : (a : Fin l →₀ R) → Fin k →₀ R) f : Fin k →₀ R) (0 : Fin k →₀ R)].TFAE
tfae_have₃ :
  ∀
    (tfae_1_iff_2 :
      Flat R M ↔
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M))
    (tfae_3_iff_2 :
      (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x) ↔
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M)),
    [Flat R M,
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M),
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x,
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x,
        ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
          Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M) →
            ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
              x = y ∘ₗ a ∧
                Eq (α := Fin k →₀ R) ((a : (a : Fin l →₀ R) → Fin k →₀ R) f : Fin k →₀ R) (0 : Fin k →₀ R)].TFAE
tfae_have₄ :
  ∀
    (tfae_1_iff_2 :
      Flat R M ↔
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M))
    (tfae_3_iff_2 :
      (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x) ↔
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M))
    (tfae_3_iff_4 :
      (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x) ↔
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x),
    [Flat R M,
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M),
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x,
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x,
        ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
          Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M) →
            ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
              x = y ∘ₗ a ∧
                Eq (α := Fin k →₀ R) ((a : (a : Fin l →₀ R) → Fin k →₀ R) f : Fin k →₀ R) (0 : Fin k →₀ R)].TFAE
tfae_have₅ :
  ∀
    (tfae_1_iff_2 :
      Flat R M ↔
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M))
    (tfae_3_iff_2 :
      (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x) ↔
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M))
    (tfae_3_iff_4 :
      (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x) ↔
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x)
    (tfae_4_to_5 :
      ∀
        (a :
          ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
            Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x)
        {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
        Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M) →
          ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
            x = y ∘ₗ a ∧ Eq (α := Fin k →₀ R) ((a : (a : Fin l →₀ R) → Fin k →₀ R) f : Fin k →₀ R) (0 : Fin k →₀ R)),
    [Flat R M,
        ∀ (I : Ideal R),
          Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
            (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M),
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x,
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x,
        ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
          Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M) →
            ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
              x = y ∘ₗ a ∧
                Eq (α := Fin k →₀ R) ((a : (a : Fin l →₀ R) → Fin k →₀ R) f : Fin k →₀ R) (0 : Fin k →₀ R)].TFAE
⊢ [Flat R M,
      ∀ (I : Ideal R),
        Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
          (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M),
      ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
        Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x,
      ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
        Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x,
      ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
        Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M) →
          ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
            x = y ∘ₗ a ∧
              Eq (α := Fin k →₀ R) ((a : (a : Fin l →₀ R) → Fin k →₀ R) f : Fin k →₀ R) (0 : Fin k →₀ R)].TFAE
have tfae_have₆ : ∀
  (tfae_1_iff_2 :
    Flat R M ↔
      ∀ (I : Ideal R),
        Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
          (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M))
  (tfae_3_iff_2 :
    (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
        Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x) ↔
      ∀ (I : Ideal R),
        Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
          (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M))
  (tfae_3_iff_4 :
    (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
        Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x) ↔
      ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
        Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x)
  (tfae_4_to_5 :
    ∀
      (a :
        ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
          Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x)
      {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
      Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M) →
        ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
          x = y ∘ₗ a ∧ Eq (α := Fin k →₀ R) ((a : (a : Fin l →₀ R) → Fin k →₀ R) f : Fin k →₀ R) (0 : Fin k →₀ R))
  (tfae_5_to_4 :
    ∀
      (a :
        ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
          Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M) →
            ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
              x = y ∘ₗ a ∧ Eq (α := Fin k →₀ R) ((a : (a : Fin l →₀ R) → Fin k →₀ R) f : Fin k →₀ R) (0 : Fin k →₀ R))
      {l : ℕ} {f : Fin l → R} {x : Fin l → M},
      Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x),
  [Flat R M,
      ∀ (I : Ideal R),
        Function.Injective (α := ↥I ⊗[R] M) (β := R ⊗[R] M)
          (⇑(rTensor M (Submodule.subtype I)) : (a : ↥I ⊗[R] M) → R ⊗[R] M),
      ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
        Eq (α := R ⊗[R] M) (∑ i : Fin l, f i ⊗ₜ[R] x i) 0 → VanishesTrivially R f x,
      ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M},
        Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0 → IsTrivialRelation f x,
      ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
        Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M) →
          ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
            x = y ∘ₗ a ∧
              Eq (α := Fin k →₀ R) ((a : (a : Fin l →₀ R) → Fin k →₀ R) f : Fin k →₀ R) (0 : Fin k →₀ R)].TFAE
Tactic: classical
  tfae_have 1 ↔ 2 := iff_rTensor_injective'
  tfae_have 3 ↔ 2 := forall_vanishesTrivially_iff_forall_rTensor_injective R
  tfae_have 3 ↔ 4 := by
    simp [(TensorProduct.lid R M).injective.eq_iff.symm, isTrivialRelation_iff_vanishesTrivially]
  tfae_have 4 → 5
  | h₄, l, f, x, hfx => by
    let f' : Fin l → R := f
    let x' : Fin l → M := fun i ↦ x (single i 1)
    have := calc
      ∑ i, f' i • x' i
      _ = ∑ i, f i • x (single i 1) := rfl
      _ = x (∑ i, f i • Finsupp.single i 1) := by simp_rw [map_sum, map_smul]
      _ = x f := by simp_rw [smul_single, smul_eq_mul, mul_one, univ_sum_single]
      _ = 0 := hfx
    obtain ⟨k, a', y', ⟨ha'y', ha'⟩⟩ := h₄ this
    use k
    use Finsupp.linearCombination R (fun i ↦ equivFunOnFinite.symm (a' i))
    use Finsupp.linearCombination R y'
    constructor
    · apply Finsupp.basisSingleOne.ext
      intro i
      simpa [linearCombination_apply, sum_fintype, Finsupp.single_apply] using ha'y' i
    · ext j
      simp only [linearCombination_apply, zero_smul, implies_true, sum_fintype, finsetSum_apply]
      exact ha' j
  tfae_have 5 → 4
  | h₅, l, f, x, hfx => by
    let f' : Fin l →₀ R := equivFunOnFinite.symm f
    let x' : (Fin l →₀ R) →ₗ[R] M := Finsupp.linearCombination R x
    have : x' f' = 0 := by simpa [x', f', linearCombination_apply, sum_fintype] using hfx
    obtain ⟨k, a', y', ha'y', ha'⟩ := h₅ this
    refine ⟨k, fun i ↦ a' (single i 1), fun j ↦ y' (single j 1), fun i ↦ ?_, fun j ↦ ?_⟩
    · simpa [x', ← map_smul, ← map_sum, smul_single] using
        LinearMap.congr_fun ha'y' (Finsupp.single i 1)
    · simp_rw [← smul_eq_mul, ← Finsupp.smul_apply, ← map_smul, ← finsetSum_apply, ← map_sum,
        smul_single, smul_eq_mul, mul_one,
        ← (fun _ ↦ equivFunOnFinite_symm_apply_apply _ _ : ∀ x, f' x = f x), univ_sum_single]
      simpa using DFunLike.congr_fun ha' j
  tfae_finish