no goals
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
x : M
⊢ x ∈ S ↔ ∃ s, x = s • generator S
simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]