Finite generation from a finite remainder module

This is the commutative-algebra skeleton of Rückert's induction. If an ideal contains an element p and reduction modulo p lands in a Noetherian module, then finitely many lifted remainders together with p generate the ideal.

theorem LocalComplexGeometry.Ideal.fg_of_remainder_kernel {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [CommRing A] [AddCommGroup M] [Algebra R A] [Module R M] [IsNoetherian R M] (I : Ideal A) (p : A) (hp : p ∈ I) (rem : A →ₗ[R] M) (hker : rem.ker ≤ Submodule.restrictScalars R (Ideal.span {p})) : I.FG