case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
constructor
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤
intro H
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ Submodule.span R {e} = ⊥ ∨ Submodule.span R {e} = ⊤
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤
obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 0 ∨ span {e} = ⊤
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ Submodule.span R {e} = ⊥ ∨ Submodule.span R {e} = ⊤
simp only [Ideal.submodule_span_eq, Ideal.span_singleton_eq_bot]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 1 → span {e} = ⊤
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 0 ∨ span {e} = ⊤
apply Or.imp id _ (IsIdempotentElem.iff_eq_zero_or_one.mp he)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
he : IsIdempotentElem 1
h : FG (Submodule.span R {1})
H : IsIdempotentElem (Submodule.span R {1})
⊢ span {1} = ⊤
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 1 → span {e} = ⊤
rintro rfl
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
he : IsIdempotentElem 1
h : FG (Submodule.span R {1})
H : IsIdempotentElem (Submodule.span R {1})
⊢ span {1} = ⊤
simp
no goals
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I
rintro (rfl | rfl) <;> simp [IsIdempotentElem]