-- Mathlib/RingTheory/Flat/EquationalCriterion.lean
theorem exists_factorization_of_comp_eq_zero_of_free [Flat R M] {K N : Type*} [AddCommGroup K]
    [Module R K] [Module.Finite R K] [AddCommGroup N] [Module R N] [Free R N] [Module.Finite R N]
    {f : K →ₗ[R] N} {x : N →ₗ[R] M} (h : x ∘ₗ f = 0) :
    ∃ (k : ℕ) (a : N →ₗ[R] (Fin k →₀ R)) (y : (Fin k →₀ R) →ₗ[R] M),
      x = y ∘ₗ a ∧ a ∘ₗ f = 0 :=
  have e := ((Module.Free.chooseBasis R N).reindex (Fintype.equivFin _)).repr.symm
  have ⟨k, a, y, hya, haf⟩ := exists_factorization_of_comp_eq_zero_of_free_aux
    (f := e.symm ∘ₗ f) (x := x ∘ₗ e.toLinearMap) (by ext; simpa [comp_assoc] using congr($h _))
  ⟨k, a ∘ₗ e.symm, y, by rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm], by
    rwa [comp_assoc]⟩

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 : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
⊢ (x ∘ₗ ↑e) ∘ₗ ↑e.symm ∘ₗ f = 0

Tactic:
ext

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
N : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
x✝ : K
⊢ ((x ∘ₗ ↑e) ∘ₗ ↑e.symm ∘ₗ f) x✝ = 0 x✝

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 : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a ∘ₗ ↑e.symm ∘ₗ f = 0
⊢ x = y ∘ₗ a ∘ₗ ↑e.symm

Tactic:
rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]

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 : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a ∘ₗ ↑e.symm ∘ₗ f = 0
⊢ (a ∘ₗ ↑e.symm) ∘ₗ f = 0

Tactic:
rwa [comp_assoc]

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
N : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
x✝ : K
⊢ ((x ∘ₗ ↑e) ∘ₗ ↑e.symm ∘ₗ f) x✝ = 0 x✝

Tactic:
simpa [comp_assoc] using congr($h _)

Result:
no goals