awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι : Type u_3
inst_3 : Fintype ι
f : ι → R
x : ι → M
κ : Type u_4
inst_4 : Fintype κ
e : κ ≃ ι
⊢ IsTrivialRelation.{u_1, u_2, u_4} (ι := κ) (f ∘ (⇑e : (a : κ) → ι)) (x ∘ (⇑e : (a : κ) → ι)) ↔ IsTrivialRelation f x
have simp_rw : VanishesTrivially.{u_1, u_1, u_2, u_4} R (ι := κ) (f ∘ (⇑e : (a : κ) → ι)) (x ∘ (⇑e : (a : κ) → ι)) ↔
  VanishesTrivially R f x
Tactic: simp_rw [isTrivialRelation_iff_vanishesTrivially, e.vanishesTrivially_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.EquationalCriterion (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module 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
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)
Tactic: tfae_have 1 ↔ 2 := iff_rTensor_injective'
-- Lean 4 proof step from Mathlib.RingTheory.Flat.EquationalCriterion (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
have 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)
Tactic: tfae_have 3 ↔ 2 := forall_vanishesTrivially_iff_forall_rTensor_injective R
-- Lean 4 proof step from Mathlib.RingTheory.Flat.EquationalCriterion (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
have 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
Tactic: tfae_have 3 ↔ 4 := by
    simp [(TensorProduct.lid R M).injective.eq_iff.symm, isTrivialRelation_iff_vanishesTrivially]
-- 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_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
h₄ : ∀ {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
hfx : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M)
f' : Fin l → R := (⇑f : (a : Fin l) → R)
x' : Fin l → M := fun (i : Fin l) ↦ (x : (a : Fin l →₀ R) → M) (Finsupp.single i 1)
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i : Fin l,
        HSMul.hSMul (α := R) (β := M) ((f : (a : Fin l) → R) i : R)
          ((x : (a : Fin l →₀ R) → M) (Finsupp.single i 1) : M) :
      M)
    ((x : (a : Fin l →₀ R) → M)
        (∑ i : Fin l, HSMul.hSMul (α := R) (β := Fin l →₀ R) ((f : (a : Fin l) → R) i : R) (Finsupp.single i 1)) :
      M)
have simp_rw : Eq.{u_2 + 1} (α := M)
  (∑ i : Fin l,
    HSMul.hSMul (α := R) (β := M) ((f : (a : Fin l) → R) i : R) ((x : (a : Fin l →₀ R) → M) (Finsupp.single i 1) : M))
  (∑ x_1 : Fin l,
    (x : (a : Fin l →₀ R) → M)
      (HSMul.hSMul (α := R) (β := Fin l →₀ R) ((f : (a : Fin l) → R) x_1 : R) (Finsupp.single x_1 1)))
Tactic: simp_rw [map_sum, map_smul]
-- 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_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
h₄ : ∀ {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
hfx : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M)
f' : Fin l → R := (⇑f : (a : Fin l) → R)
x' : Fin l → M := fun (i : Fin l) ↦ (x : (a : Fin l →₀ R) → M) (Finsupp.single i 1)
⊢ Eq.{u_2 + 1} (α := M)
    ((x : (a : Fin l →₀ R) → M)
        (∑ i : Fin l, HSMul.hSMul (α := R) (β := Fin l →₀ R) ((f : (a : Fin l) → R) i : R) (Finsupp.single i 1)) :
      M)
    ((x : (a : Fin l →₀ R) → M) f : M)
have simp_rw : Eq.{u_2 + 1} (α := M)
  ((x : (a : Fin l →₀ R) → M)
      (∑ x : Fin l, Finsupp.single x (HSMul.hSMul (α := R) (β := R) ((f : (a : Fin l) → R) x : R) 1)) :
    M)
  ((x : (a : Fin l →₀ R) → M) f : M)
Tactic: simp_rw [smul_single, smul_eq_mul, mul_one, univ_sum_single]
-- 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_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
h₄ : ∀ {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
hfx : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M)
f' : Fin l → R := (⇑f : (a : Fin l) → R)
x' : Fin l → M := fun (i : Fin l) ↦ (x : (a : Fin l →₀ R) → M) (Finsupp.single i 1)
simp_rw :
  Eq.{u_2 + 1} (α := M)
    ((x : (a : Fin l →₀ R) → M)
        (∑ x : Fin l, Finsupp.single x (HSMul.hSMul (α := R) (β := R) ((f : (a : Fin l) → R) x : R) 1)) :
      M)
    ((x : (a : Fin l →₀ R) → M) f : M)
⊢ Eq.{u_2 + 1} (α := M)
    ((x : (a : Fin l →₀ R) → M)
        (∑ i : Fin l, HSMul.hSMul (α := R) (β := Fin l →₀ R) ((f : (a : Fin l) → R) i : R) (Finsupp.single i 1)) :
      M)
    ((x : (a : Fin l →₀ R) → M) f : M)
have simp_rw₁ : Eq.{u_2 + 1} (α := M)
  ((x : (a : Fin l →₀ R) → M)
      (∑ x : Fin l, Finsupp.single x (HMul.hMul (α := R) (β := R) ((f : (a : Fin l) → R) x : R) (1 : R))) :
    M)
  ((x : (a : Fin l →₀ R) → M) f : M)
Tactic: simp_rw [smul_single, smul_eq_mul, mul_one, univ_sum_single]
-- 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_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
h₄ : ∀ {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
hfx : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M)
f' : Fin l → R := (⇑f : (a : Fin l) → R)
x' : Fin l → M := fun (i : Fin l) ↦ (x : (a : Fin l →₀ R) → M) (Finsupp.single i 1)
simp_rw :
  Eq.{u_2 + 1} (α := M)
    ((x : (a : Fin l →₀ R) → M)
        (∑ x : Fin l, Finsupp.single x (HSMul.hSMul (α := R) (β := R) ((f : (a : Fin l) → R) x : R) 1)) :
      M)
    ((x : (a : Fin l →₀ R) → M) f : M)
simp_rw₁ :
  Eq.{u_2 + 1} (α := M)
    ((x : (a : Fin l →₀ R) → M)
        (∑ x : Fin l, Finsupp.single x (HMul.hMul (α := R) (β := R) ((f : (a : Fin l) → R) x : R) (1 : R))) :
      M)
    ((x : (a : Fin l →₀ R) → M) f : M)
⊢ Eq.{u_2 + 1} (α := M)
    ((x : (a : Fin l →₀ R) → M)
        (∑ i : Fin l, HSMul.hSMul (α := R) (β := Fin l →₀ R) ((f : (a : Fin l) → R) i : R) (Finsupp.single i 1)) :
      M)
    ((x : (a : Fin l →₀ R) → M) f : M)
have simp_rw₂ : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) (∑ x : Fin l, Finsupp.single x ((f : (a : Fin l) → R) x)) : M)
  ((x : (a : Fin l →₀ R) → M) f : M)
Tactic: simp_rw [smul_single, smul_eq_mul, mul_one, univ_sum_single]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.EquationalCriterion (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
h₄ : ∀ {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
hfx : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M)
f' : Fin l → R := (⇑f : (a : Fin l) → R)
x' : Fin l → M := fun (i : Fin l) ↦ (x : (a : Fin l →₀ R) → M) (Finsupp.single i 1)
⊢ ∃ (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)
have this : Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f' i • x' i) 0
Tactic: 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
-- 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_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
h₄ : ∀ {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
hfx : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M)
f' : Fin l → R := (⇑f : (a : Fin l) → R)
x' : Fin l → M := fun (i : Fin l) ↦ (x : (a : Fin l →₀ R) → M) (Finsupp.single i 1)
this : Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f' i • x' i) 0
⊢ ∃ (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)
have obtain : ∀ (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), Eq.{u_1 + 1} (α := R) (∑ i : Fin l, f' i * a' i j) 0),
  ∃ (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)
Tactic: obtain ⟨k, a', y', ⟨ha'y', ha'⟩⟩ := h₄ this
-- 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_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
h₄ : ∀ {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
hfx : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M)
f' : Fin l → R := (⇑f : (a : Fin l) → R)
x' : Fin l → M := fun (i : Fin l) ↦ (x : (a : Fin l →₀ R) → M) (Finsupp.single i 1)
this : Eq.{u_2 + 1} (α := M) (∑ 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), Eq.{u_1 + 1} (α := R) (∑ i : Fin l, f' i * a' i j) 0
⊢ ∃ (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)
have h : ∃ (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)
Tactic: use k
-- 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_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
h₄ : ∀ {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
hfx : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M)
f' : Fin l → R := (⇑f : (a : Fin l) → R)
x' : Fin l → M := fun (i : Fin l) ↦ (x : (a : Fin l →₀ R) → M) (Finsupp.single i 1)
this : Eq.{u_2 + 1} (α := M) (∑ 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), Eq.{u_1 + 1} (α := R) (∑ i : Fin l, f' i * a' i j) 0
⊢ ∃ (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)
have h : ∃ (y : (Fin k →₀ R) →ₗ[R] M),
  (x = y ∘ₗ linearCombination R fun (i : Fin l) ↦ (Equiv.symm equivFunOnFinite : (a : Fin k → R) → Fin k →₀ R) (a' i)) ∧
    Eq (α := Fin k →₀ R)
      ((linearCombination R fun (i : Fin l) ↦ (Equiv.symm equivFunOnFinite : (a : Fin k → R) → Fin k →₀ R) (a' i) :
            (a : Fin l →₀ R) → Fin k →₀ R)
          f :
        Fin k →₀ R)
      (0 : Fin k →₀ R)
Tactic: use Finsupp.linearCombination R (fun i ↦ equivFunOnFinite.symm (a' i))
-- 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_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
h₄ : ∀ {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
hfx : Eq.{u_2 + 1} (α := M) ((x : (a : Fin l →₀ R) → M) f : M) (0 : M)
f' : Fin l → R := (⇑f : (a : Fin l) → R)
x' : Fin l → M := fun (i : Fin l) ↦ (x : (a : Fin l →₀ R) → M) (Finsupp.single i 1)
this : Eq.{u_2 + 1} (α := M) (∑ 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), Eq.{u_1 + 1} (α := R) (∑ i : Fin l, f' i * a' i j) 0
⊢ ∃ (y : (Fin k →₀ R) →ₗ[R] M),
    (x =
        y ∘ₗ
          linearCombination R fun (i : Fin l) ↦ (Equiv.symm equivFunOnFinite : (a : Fin k → R) → Fin k →₀ R) (a' i)) ∧
      Eq (α := Fin k →₀ R)
        ((linearCombination R fun (i : Fin l) ↦ (Equiv.symm equivFunOnFinite : (a : Fin k → R) → Fin k →₀ R) (a' i) :
              (a : Fin l →₀ R) → Fin k →₀ R)
            f :
          Fin k →₀ R)
        (0 : Fin k →₀ R)
have h : (x =
    linearCombination R y' ∘ₗ
      linearCombination R fun (i : Fin l) ↦ (Equiv.symm equivFunOnFinite : (a : Fin k → R) → Fin k →₀ R) (a' i)) ∧
  Eq (α := Fin k →₀ R)
    ((linearCombination R fun (i : Fin l) ↦ (Equiv.symm equivFunOnFinite : (a : Fin k → R) → Fin k →₀ R) (a' i) :
          (a : Fin l →₀ R) → Fin k →₀ R)
        f :
      Fin k →₀ R)
    (0 : Fin k →₀ R)
Tactic: use Finsupp.linearCombination R y'