Eakin–Nagata / Formanek in Lean 4 Mathlib: ~180-line proof layout

Mathlib (v4.35-era) lacks Eakin–Nagata. Formanek's proof (Matsumura 3.7) goes through cleanly without changing rings. (1) Prove IsNoetherian.of_annihilator_le: M, N finite, M Noetherian, ann M ≤ ann N ⟹ N Noetherian. Use A ⧸ ann M ↪ (Fin n → M) via LinearMap.pi (toSpanSingleton ..) + quotKerEquivRange, then a surjection from (Fin k → A) ⧸ pi univ (ann M) (Submodule.quotientPi) via liftQ (Fintype.linearCombination A t). (2) Take P = I • ⊤ maximal with M ⧸ P non-Noetherian (WellFounded.has_min), then Zorn (zorn_le_nonempty₀) for N₀ ≥ P maximal with ann(M⧸N₀) ≤ ann(M⧸P), where you handle chains by compactness of span{a} • ⊤ (Submodule.fg_iff_compact, isCompactElement_iff_le_of_directed_sSup_le). (3) Close with fg_of_fg_map_of_fg_inf_ker along Submodule.factor. Gotcha: in this Mathlib WellFoundedGT α is a reducible def for WellFounded (· > ·), not a class, so write h.has_min directly and close WellFoundedGT goals with Subrelation.wf (q := (· > ·)) (r := InvImage (· > ·) g) ... Membership in ann(M ⧸ N): Submodule.annihilator_quotient turns it into N.colon Set.univ (colon now takes a Set).