no goals
R : Type u
M : Type v
S : Type u_1
N : Type ?u.185417
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Ring S
inst✝¹ : Module R M
inst✝ : Module R N
f : R →+* S
hf : Surjective ↑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ I = Submodule.span S {↑f (IsPrincipal.generator (comap f I))}
rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span,
  Ideal.span_singleton_generator, Ideal.map_comap_of_surjective f hf]