-- Mathlib/RingTheory/Flat/EquationalCriterion.lean
theorem exists_factorization_of_comp_eq_zero_of_free_aux [Flat R M] {K : Type*} {n : ℕ}
    [AddCommGroup K] [Module R K] [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

Proof state:
case h₂.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
K : Type u_3
inst✝² : AddCommGroup K
inst✝¹ : Module R K
inst✝ : Module.Finite R K
K' : Submodule R K
hK' : K'.FG
K₁ K₂ : Submodule R K
ih₁ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M}, x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ K₁ ≤ ker (a ∘ₗ f)
ih₂ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M}, x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ K₂ ≤ ker (a ∘ₗ f)
n : ℕ
f : K →ₗ[R] Fin n →₀ R
k₁ : ℕ
a₁ : (Fin n →₀ R) →ₗ[R] Fin k₁ →₀ R
y₁ : (Fin k₁ →₀ R) →ₗ[R] M
ha₁ : K₁ ≤ ker (a₁ ∘ₗ f)
hfx : (y₁ ∘ₗ a₁) ∘ₗ f = 0
⊢ ∃ k a y, y₁ ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ ker (a ∘ₗ f)

Tactic:
have : y₁ ∘ₗ (a₁ ∘ₗ f) = 0 := by rw [← comp_assoc, hfx]

Result:
case h₂.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
K : Type u_3
inst✝² : AddCommGroup K
inst✝¹ : Module R K
inst✝ : Module.Finite R K
K' : Submodule R K
hK' : K'.FG
K₁ K₂ : Submodule R K
ih₁ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M}, x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ K₁ ≤ ker (a ∘ₗ f)
ih₂ :
  ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M}, x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ K₂ ≤ ker (a ∘ₗ f)
n : ℕ
f : K →ₗ[R] Fin n →₀ R
k₁ : ℕ
a₁ : (Fin n →₀ R) →ₗ[R] Fin k₁ →₀ R
y₁ : (Fin k₁ →₀ R) →ₗ[R] M
ha₁ : K₁ ≤ ker (a₁ ∘ₗ f)
hfx : (y₁ ∘ₗ a₁) ∘ₗ f = 0
this : y₁ ∘ₗ a₁ ∘ₗ f = 0
⊢ ∃ k a y, y₁ ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ ker (a ∘ₗ f)

Proof state:
case h₁
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
K : Type u_3
inst✝² : AddCommGroup K
inst✝¹ : Module R K
inst✝ : Module.Finite R K
K' : Submodule R K
hK' : K'.FG
k : K
n : ℕ
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
hfx : x ∘ₗ f = 0
⊢ ∃ k_1 a y, x = y ∘ₗ a ∧ Submodule.span R {k} ≤ ker (a ∘ₗ f)

Tactic:
have : x (f k) = 0 := by simpa using LinearMap.congr_fun hfx k

Result:
case h₁
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
K : Type u_3
inst✝² : AddCommGroup K
inst✝¹ : Module R K
inst✝ : Module.Finite R K
K' : Submodule R K
hK' : K'.FG
k : K
n : ℕ
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
hfx : x ∘ₗ f = 0
this : x (f k) = 0
⊢ ∃ k_1 a y, x = y ∘ₗ a ∧ Submodule.span R {k} ≤ ker (a ∘ₗ f)

Proof state:
case h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_2.a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
K : Type u_3
n : ℕ
inst✝² : AddCommGroup K
inst✝¹ : Module R K
inst✝ : 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), K'.FG → ∃ k a y, x = y ∘ₗ a ∧ K' ≤ ker (a ∘ₗ f)
x✝² : ℕ
x✝¹ : (Fin n →₀ R) →ₗ[R] Fin x✝² →₀ R
x✝ : (Fin x✝² →₀ R) →ₗ[R] M
⊢ x✝¹ ∘ₗ f = 0 ↔ ⊤ ≤ ker (x✝¹ ∘ₗ f)

Tactic:
simp only [top_le_iff, ker_eq_top]

Result:
no goals

Proof state:
case h₁
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
K : Type u_3
inst✝² : AddCommGroup K
inst✝¹ : Module R K
inst✝ : Module.Finite R K
K' : Submodule R K
hK' : K'.FG
k : K
n : ℕ
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
hfx : x ∘ₗ f = 0
this : x (f k) = 0
⊢ ∃ k_1 a y, x = y ∘ₗ a ∧ Submodule.span R {k} ≤ ker (a ∘ₗ f)

Tactic:
simpa using exists_factorization_of_apply_eq_zero_of_free this

Result:
no goals