ι : Type ?u.23103
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type ?u.23295
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ span R {generator I} = Ideal.span {x}
ι : Type ?u.23103
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type ?u.23295
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ I = Ideal.span {x}
conv_rhs => rw [← span_singleton_generator I]
ι : Type ?u.23103
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type ?u.23295
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ x ∈ I ∧ x ∣ generator I
ι : Type ?u.23103
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type ?u.23295
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ span R {generator I} = Ideal.span {x}
rw [Ideal.submodule_span_eq, Ideal.span_singleton_eq_span_singleton, ← dvd_dvd_iff_associated,
  ← mem_iff_generator_dvd]
no goals
ι : Type ?u.23103
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type ?u.23295
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ x ∈ I ∧ x ∣ generator I
exact ⟨fun h ↦ ⟨hx, h⟩, fun h ↦ h.2⟩