theorem exists_lifted_prime_chain {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] (hker : RingHom.ker (algebraMap R S) = ⊥) (n : ℕ) (s : LTSeries (PrimeSpectrum R)) (hs : s.length = n) : ∃ (t : LTSeries (PrimeSpectrum S)), t.length = n ∧ Ideal.comap (algebraMap R S) (RelSeries.last t).asIdeal = (RelSeries.last s).asIdeal