awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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)
⊢ ∀
    (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

Tactic:
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
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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)
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:
tfae_finish
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ {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_equational_criterion R M).out 0 3

Premises used: List.TFAE.out, Module.Flat.tfae_equational_criterion, OfNat.ofNat
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
ι : Type u_3
inst_4 : Fintype ι
f : ι → R
x : ι → M
h : Eq.{u_2 + 1} (α := M) (∑ i : ι, f i • x i) 0
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i : Fin (Fintype.card ι),
      (f ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)) i •
        (x ∘ (⇑(Equiv.symm (Fintype.equivFin ι)) : (a : Fin (Fintype.card ι)) → ι)) i)
    0

Tactic:
simpa only [← (Fintype.equivFin ι).symm.sum_comp] using h

Premises used: Equiv.sum_comp, Fintype.equivFin, Equiv.symm
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
hfx :
  ∀ {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

Tactic:
iff_forall_isTrivialRelation.mpr hfx

Premises used: Iff.mpr, Module.Flat.iff_forall_isTrivialRelation
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ {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)

Tactic:
(tfae_equational_criterion R M).out 0 4

Premises used: List.TFAE.out, Module.Flat.tfae_equational_criterion, OfNat.ofNat
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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)
⊢ Flat R M

Tactic:
iff_forall_exists_factorization.mpr h

Premises used: Iff.mpr, Module.Flat.iff_forall_exists_factorization
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
⊢ Eq.{u_2 + 1} (α := M)
    ((x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N) :
          (a : Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) → M)
        ((e.symm : (a : N) → Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) f :
          Fin (Fintype.card.{u_3} (Free.ChooseBasisIndex R N)) →₀ R) :
      M)
    (0 : M)

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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)
rwa : x = (y ∘ₗ a) ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R)
rwa₁ rwa₂ rwa₃ rwa₄ : x ∘ₗ (↑e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] N) = y ∘ₗ a
⊢ x = y ∘ₗ a ∘ₗ (↑e.symm : N →ₗ[R] Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R)

Tactic:
rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]

Premises used: LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
⊢ 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:
simpa using LinearMap.congr_fun h k

Premises used: LinearMap.congr_fun
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
⊢ 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
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
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)
⊢ ∃ (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:
simpa using exists_factorization_of_apply_eq_zero_of_free this

Premises used: Module.Flat.exists_factorization_of_apply_eq_zero_of_free
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
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
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ (a ∘ₗ f).ker

Tactic:
obtain ⟨k₁, a₁, y₁, rfl, ha₁⟩ := ih₁ h

Premises used: rfl
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
rw₁ rw₂ : Eq (α := K →ₗ[R] M) 0 0
⊢ y₁ ∘ₗ a₁ ∘ₗ f = 0

Tactic:
rw [← comp_assoc, h]

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
⊢ y₁ ∘ₗ a₁ ∘ₗ f = 0

Tactic:
have : y₁ ∘ₗ (a₁ ∘ₗ f) = 0 := by rw [← comp_assoc, h]
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
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
⊢ ∃ (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₂ this

Premises used: rfl
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
h₁ : (y₂ ∘ₗ a₂) ∘ₗ a₁ = y₂ ∘ₗ a₂ ∘ₗ a₁ ∧ K₁ ⊔ K₂ ≤ ((a₂ ∘ₗ a₁) ∘ₗ f).ker
⊢ ∃ (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:
use k₂, a₂ ∘ₗ a₁, y₂
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
h₁ : True ∧ K₁ ⊔ K₂ ≤ (a₂ ∘ₗ a₁ ∘ₗ f).ker
⊢ (y₂ ∘ₗ a₂) ∘ₗ a₁ = y₂ ∘ₗ a₂ ∘ₗ a₁ ∧ K₁ ⊔ K₂ ≤ ((a₂ ∘ₗ a₁) ∘ₗ f).ker

Tactic:
simp_rw [comp_assoc]

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
⊢ True ∧ K₁ ⊔ K₂ ≤ (a₂ ∘ₗ a₁ ∘ₗ f).ker

Tactic:
⟨trivial, sup_le (ha₁.trans (ker_le_ker_comp _ _)) ha₂⟩

Premises used: trivial, And.intro, sup_le, LinearMap.ker_le_ker_comp, LE.le.trans
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
⊢ True ∧ K₁ ⊔ K₂ ≤ (a₂ ∘ₗ a₁ ∘ₗ f).ker

Tactic:
exact ⟨trivial, sup_le (ha₁.trans (ker_le_ker_comp _ _)) ha₂⟩
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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
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
⊢ ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] Fin k →₀ R) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ 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₂⟩

Premises used: LinearMap.comp_assoc, Submodule.fg_induction, Singleton.singleton, rfl
-- Module: Mathlib.RingTheory.Flat.EquationalCriterion
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

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₂⟩