-- 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₂
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
x : (Fin n →₀ R) →ₗ[R] M
hfx : x ∘ₗ f = 0
⊢ ∃ k a y, x = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ ker (a ∘ₗ f)

Tactic:
obtain ⟨k₁, a₁, y₁, rfl, ha₁⟩ := ih₁ 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
⊢ ∃ k a y, y₁ ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ ker (a ∘ₗ f)

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
this : y₁ ∘ₗ a₁ ∘ₗ f = 0
⊢ ∃ k a y, y₁ ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ ker (a ∘ₗ f)

Tactic:
obtain ⟨k₂, a₂, y₂, rfl, ha₂⟩ := ih₂ this

Result:
case h₂.intro.intro.intro.intro.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
ha₁ : K₁ ≤ ker (a₁ ∘ₗ f)
k₂ : ℕ
a₂ : (Fin k₁ →₀ R) →ₗ[R] Fin k₂ →₀ R
y₂ : (Fin k₂ →₀ R) →ₗ[R] M
ha₂ : K₂ ≤ ker (a₂ ∘ₗ a₁ ∘ₗ f)
hfx : ((y₂ ∘ₗ a₂) ∘ₗ a₁) ∘ₗ f = 0
this : (y₂ ∘ₗ a₂) ∘ₗ a₁ ∘ₗ f = 0
⊢ ∃ k a y, (y₂ ∘ₗ a₂) ∘ₗ a₁ = y ∘ₗ a ∧ K₁ ⊔ K₂ ≤ ker (a ∘ₗ f)

Proof state:
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
⊢ y₁ ∘ₗ a₁ ∘ₗ f = 0

Tactic:
rw [← comp_assoc, hfx]

Result:
no goals

Proof state:
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
⊢ ∀ {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)

Tactic:
apply Submodule.fg_induction (N := K') (hN := hK')

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
⊢ ∀ (x : K) {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x_1 : (Fin n →₀ R) →ₗ[R] M},
    x_1 ∘ₗ f = 0 → ∃ k a y, x_1 = y ∘ₗ a ∧ Submodule.span R {x} ≤ ker (a ∘ₗ f)

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
⊢ ∀ (M₁ M₂ : Submodule R K),
    (∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M},
        x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ M₁ ≤ ker (a ∘ₗ f)) →
      (∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M},
          x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ M₂ ≤ ker (a ∘ₗ f)) →
        ∀ {n : ℕ} {f : K →ₗ[R] Fin n →₀ R} {x : (Fin n →₀ R) →ₗ[R] M},
          x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ M₁ ⊔ M₂ ≤ ker (a ∘ₗ f)

Proof state:
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
⊢ x (f k) = 0

Tactic:
simpa using LinearMap.congr_fun hfx k

Result:
no goals

Proof state:
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
K' : Submodule R K
hK' : K'.FG
⊢ ∃ k a y, x = y ∘ₗ a ∧ K' ≤ ker (a ∘ₗ f)

Tactic:
revert n

Result:
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
⊢ ∀ {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)