theorem span_union_eq_top_of_powers {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {f g : A} (hfg : Ideal.span {f, g} = ⊤) {S T : Set M} {n k : ℕ} (hS : ∀ (m : M), f ^ n • m ∈ Submodule.span A S) (hT : ∀ (m : M), g ^ k • m ∈ Submodule.span A T) : Submodule.span A (S ∪ T) = ⊤

If (f, g) = (1) in A and every f^n • m lies in span S while every g^k • m lies in span T, then S ∪ T spans all of M. A gluing helper for local-to-global finite generation arguments behind quasi-coherence.

theorem module_fg_of_localization_fg {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {f g : A} (hfg : Ideal.span {f, g} = ⊤) {S T : Set M} (hSfin : S.Finite) (hTfin : T.Finite) {n k : ℕ} (hS : ∀ (m : M), f ^ n • m ∈ Submodule.span A S) (hT : ∀ (m : M), g ^ k • m ∈ Submodule.span A T) : Module.Finite A M

Lem 23 / coherence helper: if (f, g) = (1) and M is generated by a finite set after inverting f (resp. g), then M is itself finitely generated as an A-module.