-- Mathlib/RingTheory/Ideal/IdempotentFG.lean
theorem isIdempotentElem_iff_of_fg {R : Type*} [CommRing R] (I : Ideal R) (h : I.FG) :
    IsIdempotentElem I ↔ ∃ e : R, IsIdempotentElem e ∧ I = R ∙ e

Proof state:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
⊢ I ≤ Submodule.span R {r}

Tactic:
intro x hx

Result:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ x ∈ Submodule.span R {r}

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

Tactic:
intro e

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

Proof state:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r • n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}

Tactic:
simp_rw [smul_eq_mul] at hr'

Result:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}

Proof state:
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})

Tactic:
simp [IsIdempotentElem, Ideal.span_singleton_mul_span_singleton, he.eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ I ≤ I • I

Tactic:
rw [smul_eq_mul]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ I ≤ I * I

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

Tactic:
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)

Result:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r • n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ I ≤ I * I

Tactic:
exact e.ge

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ r * x ∈ Submodule.span R {r}

Tactic:
exact Ideal.mem_span_singleton'.mpr ⟨_, mul_comm _ _⟩

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ x ∈ Submodule.span R {r}

Tactic:
rw [← hr' x hx]

Result:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ r * x ∈ Submodule.span R {r}

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I ↔ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}

Tactic:
constructor

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

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

Proof state:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}

Tactic:
refine ⟨r, hr' r hr, antisymm ?_ ((Submodule.span_singleton_le_iff_mem _ _).mpr hr)⟩

Result:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
⊢ I ≤ Submodule.span R {r}

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

Tactic:
rintro ⟨e, he, rfl⟩

Result:
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})