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

Tactic:
simp_rw [comp_assoc]

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₂ : 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
⊢ True ∧ K₁ ⊔ K₂ ≤ ker (a₂ ∘ₗ a₁ ∘ₗ f)

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

Tactic:
use k₂, a₂ ∘ₗ a₁, y₂

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₂ : 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
⊢ (y₂ ∘ₗ a₂) ∘ₗ a₁ = y₂ ∘ₗ a₂ ∘ₗ a₁ ∧ K₁ ⊔ K₂ ≤ ker ((a₂ ∘ₗ 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
⊢ ∀ (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)

Tactic:
intro k n f x hfx

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
⊢ ∃ k_1 a y, x = y ∘ₗ a ∧ Submodule.span R {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
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)
⊢ ∃ k a y, x = y ∘ₗ a ∧ a ∘ₗ f = 0

Tactic:
convert this ⊤ Finite.fg_top

Result:
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)

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
⊢ ∀ (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)

Tactic:
intro K₁ K₂ ih₁ ih₂ n f x hfx

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₂ : 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)

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
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
⊢ True ∧ K₁ ⊔ K₂ ≤ ker (a₂ ∘ₗ a₁ ∘ₗ f)

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

Result:
no goals