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
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)
h₅ :
  ∀ {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
hfx : Eq.{u_2 + 1} (α := M) (∑ i : Fin l, f i • x i) 0
f' : Fin l →₀ R := (Equiv.symm equivFunOnFinite : (a : Fin l → R) → Fin l →₀ R) f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
this : 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
ha'y' : x' = y' ∘ₗ a'
ha' : Eq (α := Fin k →₀ R) ((a' : (a : Fin l →₀ R) → Fin k →₀ R) f' : Fin k →₀ R) (0 : Fin k →₀ R)
j : Fin k
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i : Fin l,
      f i *
        (fun (i : Fin l) ↦
            ((⇑((a' : (a : Fin l →₀ R) → Fin k →₀ R) (Finsupp.single i 1) : Fin k →₀ R) : (a : Fin k) → R) :
              (a : Fin k) → R))
          i j)
    0
have refine_2 : Eq (α := R)
  ((((a' : (a : Fin l →₀ R) → Fin k →₀ R) ((Equiv.symm equivFunOnFinite : (a : Fin l → R) → Fin l →₀ R) f) :
          Fin k →₀ R) :
        (a : Fin k) → R)
      j :
    R)
  (0 : R)
Tactic: 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]
-- 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
inst_3 : Flat R M
N : Type u_3
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : Free R N
inst_7 : Module.Finite R N
f : N
x : N →ₗ[R] M
h : Eq.{u_2 + 1} (α := M) ((x : (a : N) → M) f : M) (0 : M)
e : (Fin (Fintype.card.{u_3} (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card.{u_3} (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N) = y ∘ₗ a
haf :
  Eq (α := Fin k →₀ R)
    ((a : (a : Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) → Fin k →₀ R)
        ((e.symm : (a : N) → Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) f) :
      Fin k →₀ R)
    (0 : Fin k →₀ R)
⊢ x = y ∘ₗ a ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R)
have rwa : x = (y ∘ₗ a) ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R)
Tactic: rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]
-- 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
inst_3 : Flat R M
K : Type u_3
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
K' : Submodule R K
k : K
n : ℕ
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
⊢ ∃ (k_1 : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k_1 →₀ R) (y : (Fin k_1 →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ R ∙ k ≤ (a ∘ₗ f).ker
have this : Eq.{u_2 + 1} (α := M) ((x : (a : Fin n →₀ R) → M) ((f : (a : K) → Fin n →₀ R) k : Fin n →₀ R) : M) (0 : M)
Tactic: have : x (f k) = 0 := by simpa using LinearMap.congr_fun h 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
inst_3 : Flat R M
K : Type u_3
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
K' K₁ K₂ : Submodule R K
hN₁ : K₁.FG
hN₂ : K₂.FG
ih₁ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ≤ (a ∘ₗ f).ker
ih₂ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₂ ≤ (a ∘ₗ f).ker
n : ℕ
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ (a ∘ₗ f).ker
have sup : ∀ (k₁ : ℕ) (a₁ : (Fin n →₀ R) →ₗ[R] Fin k₁ →₀ R) (y₁ : (Fin k₁ →₀ R) →ₗ[R] M) (ha₁ : K₁ ≤ (a₁ ∘ₗ f).ker)
  (h : (y₁ ∘ₗ a₁) ∘ₗ f = 0),
  ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), y₁ ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ (a ∘ₗ f).ker
Tactic: obtain ⟨k₁, a₁, y₁, rfl, ha₁⟩ := ih₁ h
Cleared hypotheses: x, h
-- 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
inst_3 : Flat R M
K : Type u_3
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
K' K₁ K₂ : Submodule R K
hN₁ : K₁.FG
hN₂ : K₂.FG
ih₁ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ≤ (a ∘ₗ f).ker
ih₂ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₂ ≤ (a ∘ₗ f).ker
n : ℕ
f : K →ₗ[R] Fin n →₀ R
k₁ : ℕ
a₁ : (Fin n →₀ R) →ₗ[R] Fin k₁ →₀ R
y₁ : (Fin k₁ →₀ R) →ₗ[R] M
ha₁ : K₁ ≤ (a₁ ∘ₗ f).ker
h rw : (y₁ ∘ₗ a₁) ∘ₗ f = 0
⊢ y₁ ∘ₗ a₁ ∘ₗ f = 0
have rw₁ : Eq (α := K →ₗ[R] M) 0 0
Tactic: rw [← comp_assoc, h]
-- 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
inst_3 : Flat R M
K : Type u_3
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
K' K₁ K₂ : Submodule R K
hN₁ : K₁.FG
hN₂ : K₂.FG
ih₁ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ≤ (a ∘ₗ f).ker
ih₂ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₂ ≤ (a ∘ₗ f).ker
n : ℕ
f : K →ₗ[R] Fin n →₀ R
k₁ : ℕ
a₁ : (Fin n →₀ R) →ₗ[R] Fin k₁ →₀ R
y₁ : (Fin k₁ →₀ R) →ₗ[R] M
ha₁ : K₁ ≤ (a₁ ∘ₗ f).ker
h : (y₁ ∘ₗ a₁) ∘ₗ f = 0
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), y₁ ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ (a ∘ₗ f).ker
have this : y₁ ∘ₗ a₁ ∘ₗ f = 0
Tactic: have : y₁ ∘ₗ (a₁ ∘ₗ f) = 0 := by rw [← comp_assoc, h]
-- 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
inst_3 : Flat R M
K : Type u_3
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
K' K₁ K₂ : Submodule R K
hN₁ : K₁.FG
hN₂ : K₂.FG
ih₁ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ≤ (a ∘ₗ f).ker
ih₂ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₂ ≤ (a ∘ₗ f).ker
n : ℕ
f : K →ₗ[R] Fin n →₀ R
k₁ : ℕ
a₁ : (Fin n →₀ R) →ₗ[R] Fin k₁ →₀ R
y₁ : (Fin k₁ →₀ R) →ₗ[R] M
ha₁ : K₁ ≤ (a₁ ∘ₗ f).ker
h : (y₁ ∘ₗ a₁) ∘ₗ f = 0
this : y₁ ∘ₗ a₁ ∘ₗ f = 0
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), y₁ ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ (a ∘ₗ f).ker
have sup : ∀ (k₂ : ℕ) (a₂ : (Fin k₁ →₀ R) →ₗ[R] Fin k₂ →₀ R) (y₂ : (Fin k₂ →₀ R) →ₗ[R] M) (ha₂ : K₂ ≤ (a₂ ∘ₗ a₁ ∘ₗ f).ker)
  (h : ((y₂ ∘ₗ a₂) ∘ₗ a₁) ∘ₗ f = 0) (this : (y₂ ∘ₗ a₂) ∘ₗ a₁ ∘ₗ f = 0),
  ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
    (y₂ ∘ₗ a₂) ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ (a ∘ₗ f).ker
Tactic: obtain ⟨k₂, a₂, y₂, rfl, ha₂⟩ := ih₂ this
Cleared hypotheses: y₁, 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
inst_3 : Flat R M
K : Type u_3
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
K' K₁ K₂ : Submodule R K
hN₁ : K₁.FG
hN₂ : K₂.FG
ih₁ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ≤ (a ∘ₗ f).ker
ih₂ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₂ ≤ (a ∘ₗ f).ker
n : ℕ
f : K →ₗ[R] Fin n →₀ R
k₁ : ℕ
a₁ : (Fin n →₀ R) →ₗ[R] Fin k₁ →₀ R
ha₁ : K₁ ≤ (a₁ ∘ₗ f).ker
k₂ : ℕ
a₂ : (Fin k₁ →₀ R) →ₗ[R] Fin k₂ →₀ R
y₂ : (Fin k₂ →₀ R) →ₗ[R] M
ha₂ : K₂ ≤ (a₂ ∘ₗ a₁ ∘ₗ f).ker
h : ((y₂ ∘ₗ a₂) ∘ₗ a₁) ∘ₗ f = 0
this : (y₂ ∘ₗ a₂) ∘ₗ a₁ ∘ₗ f = 0
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M),
    (y₂ ∘ₗ a₂) ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ (a ∘ₗ f).ker
have h₁ : (y₂ ∘ₗ a₂) ∘ₗ a₁ = y₂ ∘ₗ a₂ ∘ₗ a₁ ∧ K₁ ⊔ K₂ ≤ ((a₂ ∘ₗ a₁) ∘ₗ f).ker
Tactic: use k₂, a₂ ∘ₗ a₁, y₂
-- 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
inst_3 : Flat R M
K : Type u_3
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
K' K₁ K₂ : Submodule R K
hN₁ : K₁.FG
hN₂ : K₂.FG
ih₁ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ≤ (a ∘ₗ f).ker
ih₂ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₂ ≤ (a ∘ₗ f).ker
n : ℕ
f : K →ₗ[R] Fin n →₀ R
k₁ : ℕ
a₁ : (Fin n →₀ R) →ₗ[R] Fin k₁ →₀ R
ha₁ : K₁ ≤ (a₁ ∘ₗ f).ker
k₂ : ℕ
a₂ : (Fin k₁ →₀ R) →ₗ[R] Fin k₂ →₀ R
y₂ : (Fin k₂ →₀ R) →ₗ[R] M
ha₂ : K₂ ≤ (a₂ ∘ₗ a₁ ∘ₗ f).ker
h : ((y₂ ∘ₗ a₂) ∘ₗ a₁) ∘ₗ f = 0
this : (y₂ ∘ₗ a₂) ∘ₗ a₁ ∘ₗ f = 0
⊢ (y₂ ∘ₗ a₂) ∘ₗ a₁ = y₂ ∘ₗ a₂ ∘ₗ a₁ ∧ K₁ ⊔ K₂ ≤ ((a₂ ∘ₗ a₁) ∘ₗ f).ker
have h₁ : True ∧ K₁ ⊔ K₂ ≤ (a₂ ∘ₗ a₁ ∘ₗ f).ker
Tactic: simp_rw [comp_assoc]
-- 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
inst_3 : Flat R M
K : Type u_3
n : ℕ
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
K' : Submodule R K
hK' : K'.FG
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ (a ∘ₗ f).ker
have singleton : ∀ (k : K) {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
  ∃ (k_1 : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k_1 →₀ R) (y : (Fin k_1 →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ R ∙ k ≤ (a ∘ₗ f).ker
Tactic: induction K', hK' using Submodule.fg_induction generalizing n with
    | singleton k =>
      have : x (f k) = 0 := by simpa using LinearMap.congr_fun h k
      simpa using exists_factorization_of_apply_eq_zero_of_free this
    | sup K₁ K₂ _ _ ih₁ ih₂ =>
      obtain ⟨k₁, a₁, y₁, rfl, ha₁⟩ := ih₁ h
      have : y₁ ∘ₗ (a₁ ∘ₗ f) = 0 := by rw [← comp_assoc, h]
      obtain ⟨k₂, a₂, y₂, rfl, ha₂⟩ := ih₂ this
      use k₂, a₂ ∘ₗ a₁, y₂
      simp_rw [comp_assoc]
      exact ⟨trivial, sup_le (ha₁.trans (ker_le_ker_comp _ _)) ha₂⟩
Cleared hypotheses: n, f, x, h, hK'
-- 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
inst_3 : Flat R M
K : Type u_3
n : ℕ
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
K' : Submodule R K
hK' : K'.FG
singleton :
  ∀ (k : K) {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
    ∃ (k_1 : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k_1 →₀ R) (y : (Fin k_1 →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ R ∙ k ≤ (a ∘ₗ f).ker
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ (a ∘ₗ f).ker
have sup : ∀ (K₁ K₂ : Submodule R K),
  K₁.FG →
    K₂.FG →
      ∀
        (ih₁ :
          ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
            ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ≤ (a ∘ₗ f).ker)
        (ih₂ :
          ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
            ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₂ ≤ (a ∘ₗ f).ker)
        {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M} (h : x ∘ₗ f = 0),
        ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ (a ∘ₗ f).ker
Tactic: induction K', hK' using Submodule.fg_induction generalizing n with
    | singleton k =>
      have : x (f k) = 0 := by simpa using LinearMap.congr_fun h k
      simpa using exists_factorization_of_apply_eq_zero_of_free this
    | sup K₁ K₂ _ _ ih₁ ih₂ =>
      obtain ⟨k₁, a₁, y₁, rfl, ha₁⟩ := ih₁ h
      have : y₁ ∘ₗ (a₁ ∘ₗ f) = 0 := by rw [← comp_assoc, h]
      obtain ⟨k₂, a₂, y₂, rfl, ha₂⟩ := ih₂ this
      use k₂, a₂ ∘ₗ a₁, y₂
      simp_rw [comp_assoc]
      exact ⟨trivial, sup_le (ha₁.trans (ker_le_ker_comp _ _)) ha₂⟩
Cleared hypotheses: n, f, x, h, hK'
-- 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
inst_3 : Flat R M
K : Type u_3
n : ℕ
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a ∘ₗ f = 0
have this : ∀ (K' : Submodule R K) (hK' : K'.FG),
  ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ (a ∘ₗ f).ker
Tactic: have (K' : Submodule R K) (hK' : K'.FG) : ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] (Fin k →₀ R))
      (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ LinearMap.ker (a ∘ₗ f) := by
    induction K', hK' using Submodule.fg_induction generalizing n with
    | singleton k =>
      have : x (f k) = 0 := by simpa using LinearMap.congr_fun h k
      simpa using exists_factorization_of_apply_eq_zero_of_free this
    | sup K₁ K₂ _ _ ih₁ ih₂ =>
      obtain ⟨k₁, a₁, y₁, rfl, ha₁⟩ := ih₁ h
      have : y₁ ∘ₗ (a₁ ∘ₗ f) = 0 := by rw [← comp_assoc, h]
      obtain ⟨k₂, a₂, y₂, rfl, ha₂⟩ := ih₂ this
      use k₂, a₂ ∘ₗ a₁, y₂
      simp_rw [comp_assoc]
      exact ⟨trivial, sup_le (ha₁.trans (ker_le_ker_comp _ _)) ha₂⟩
-- 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
inst_3 : Flat R M
K : Type u_3
n : ℕ
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
this :
  ∀ (K' : Submodule R K) (hK' : K'.FG),
    ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ (a ∘ₗ f).ker
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a ∘ₗ f = 0
have h₁ : ∀ (x : ℕ) (x_1 : (Fin n →₀ R) →ₗ[R] Fin x →₀ R) (x_2 : (Fin x →₀ R) →ₗ[R] M), x_1 ∘ₗ f = 0 ↔ ⊤ ≤ (x_1 ∘ₗ f).ker
Tactic: convert! this ⊤ Finite.fg_top
-- 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
inst_3 : Flat R M
K : Type u_3
N : Type u_4
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Free R N
inst_10 : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card.{u_4} (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
⊢ (x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N)) ∘ₗ
      (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ∘ₗ f =
    0
have h₁ : ∀ (x_1 : K),
  Eq.{u_2 + 1} (α := M)
    (((x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N)) ∘ₗ
            (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ∘ₗ f :
          (a : K) → M)
        x_1 :
      M)
    ((0 : (a : K) → M) x_1 : M)
Tactic: ext
-- 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
inst_3 : Flat R M
K : Type u_3
N : Type u_4
inst_4 : AddCommGroup K
inst_5 : Module R K
inst_6 : Module.Finite R K
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Free R N
inst_10 : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card.{u_4} (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card.{u_4} (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N) = y ∘ₗ a
haf : a ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ∘ₗ f = 0
⊢ x = y ∘ₗ a ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R)
have rwa : x = (y ∘ₗ a) ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R)
Tactic: rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]
-- 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
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
⊢ ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂
have have : ∀ (w : ℕ) (K : Submodule R (Fin w → R)) (ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K) (hK : K.FG),
  ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂
Tactic: have ⟨_, K, ϕ, hK⟩ := FinitePresentation.exists_fin R P
-- 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
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
⊢ ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂
have this : Module.Finite R ↥K
Tactic: haveI : Module.Finite R K := .of_fg hK
-- 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
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this : Module.Finite R ↥K
⊢ (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
have simp_rw : Eq (α := ↥K →ₗ[R] M) (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ ∘ₗ K.subtype) 0
Tactic: simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]
-- 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
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this : Module.Finite R ↥K
simp_rw : Eq (α := ↥K →ₗ[R] M) (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ ∘ₗ K.subtype) 0
⊢ (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
have simp_rw₁ : Eq (α := ↥K →ₗ[R] M) (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ 0) 0
Tactic: simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]
-- 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
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this : Module.Finite R ↥K
⊢ ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂
have this₁ : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
Tactic: have : (h₁ ∘ₗ ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0 := by
    simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]
-- 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
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
⊢ ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂
have obtain : ∀ (k : ℕ) (a : (Fin w → R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M)
  (hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a) (ha : a ∘ₗ K.subtype = 0),
  ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂
Tactic: obtain ⟨k, a, y, hay, ha⟩ := exists_factorization_of_comp_eq_zero_of_free 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
inst_3 : Flat R M
P : Type u_3
inst_4 : AddCommGroup P
inst_5 : Module R P
inst_6 : FinitePresentation R P
h₁ : P →ₗ[R] M
w : ℕ
K : Submodule R (Fin w → R)
ϕ : P ≃ₗ[R] (Fin w → R) ⧸ K
hK : K.FG
this_1 : Module.Finite R ↥K
this : (h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ) ∘ₗ K.subtype = 0
k : ℕ
a : (Fin w → R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hay : h₁ ∘ₗ (↑ϕ.symm : (Fin w → R) ⧸ K →ₗ[R] P) ∘ₗ K.mkQ = y ∘ₗ a
ha : a ∘ₗ K.subtype = 0
⊢ K ≤ a.ker
have rwa : ∀ (ha : K.subtype.range ≤ a.ker), K ≤ a.ker
Tactic: rwa [← range_le_ker_iff, Submodule.range_subtype] at ha
Cleared hypotheses: ha