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