case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I → ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}

case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ (∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}) → IsIdempotentElem I
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I ↔ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
constructor
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I → ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
intro e
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r • n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
obtain ⟨r, hr, hr'⟩ :=
  Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I I h
    (by
      rw [smul_eq_mul]
      exact e.ge)
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r • n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
simp_rw [smul_eq_mul] at hr'
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
⊢ I ≤ Submodule.span R {r}
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
refine' ⟨r, hr' r hr, antisymm _ ((Submodule.span_singleton_le_iff_mem _ _).mpr hr)⟩
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
x : R
hx : x ∈ I
⊢ x ∈ Submodule.span R {r}
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
⊢ I ≤ Submodule.span R {r}
intro x hx
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
x : R
hx : x ∈ I
⊢ r * x ∈ Submodule.span R {r}
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
x : R
hx : x ∈ I
⊢ x ∈ Submodule.span R {r}
rw [← hr' x hx]
no goals
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
x : R
hx : x ∈ I
⊢ r * x ∈ Submodule.span R {r}
exact Ideal.mem_span_singleton'.mpr ⟨_, mul_comm _ _⟩
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ I ≤ I * I
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ I ≤ I • I
rw [smul_eq_mul]
no goals
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ I ≤ I * I
exact e.ge
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
⊢ IsIdempotentElem (Submodule.span R {e})
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ (∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}) → IsIdempotentElem I
rintro ⟨e, he, rfl⟩
no goals
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
⊢ IsIdempotentElem (Submodule.span R {e})
simp [IsIdempotentElem, Ideal.span_singleton_mul_span_singleton, he.eq]