Descend finiteness along quotients by nilpotent ideals

theorem Module.finite_of_surjective_of_ker_le_nilradical {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Module.Finite R T] (f : S →ₐ[R] T) (hf₁ : Function.Surjective ⇑f) (hf₂ : RingHom.ker f ≤ nilradical S) (hf₃ : (RingHom.ker f).FG) : Module.Finite R S

If I is a finitely generated nilpotent ideal of an R-algebra S, and T = S / I is R-finite, then S is also R-finite.