-- Mathlib/RingTheory/Filtration.lean
theorem Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing {R} [CommRing R]
    [IsNoetherianRing R] [IsLocalRing R] (I : Ideal R) :
    IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Proof state:
case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I ≤ ⊥

Tactic:
rw [← Ideal.iInf_pow_eq_bot_of_isLocalRing I ‹_›]

Result:
case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I ≤ ⨅ i, I ^ i

Proof state:
case pos
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : I = ⊤
⊢ I = ⊥ ∨ I = ⊤

Tactic:
exact Or.inr ‹_›

Result:
no goals

Proof state:
case mpr
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I

Tactic:
rintro (rfl | rfl) <;> simp [IsIdempotentElem]

Result:
no goals

Proof state:
case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I ≤ ⨅ i, I ^ i

Tactic:
apply le_iInf

Result:
case neg.h
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ ∀ (i : ℕ), I ≤ I ^ i

Proof state:
case mp
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤

Tactic:
intro H

Result:
case mp
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤

Proof state:
case neg.h
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ ∀ (i : ℕ), I ≤ I ^ i

Tactic:
rintro (_|n) <;> simp [H.pow_succ_eq]

Result:
no goals

Proof state:
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Tactic:
constructor

Result:
case mp
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤

case mpr
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I

Proof state:
case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I = ⊥ ∨ I = ⊤

Tactic:
refine Or.inl (eq_bot_iff.mpr ?_)

Result:
case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I ≤ ⊥

Proof state:
case mp
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤

Tactic:
by_cases I = ⊤

Result:
case pos
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : I = ⊤
⊢ I = ⊥ ∨ I = ⊤

case neg
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I = ⊥ ∨ I = ⊤