Theorem: Ideal.IsPrime.not_one_mem (FormalisingMathematics2024/Solutions/Section14UFDsAndPIDsEtc/Sheet3.lean)

State before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
⊢ 1 ∉ P
Tactic:
intro h
State after:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
h : 1 ∈ P
⊢ False

State before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
h : 1 ∈ P
⊢ False
Tactic:
apply hI.ne_top
State after:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
h : 1 ∈ P
⊢ P = ⊤

State before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
h : 1 ∈ P
⊢ P = ⊤
Tactic:
rwa [Ideal.eq_top_iff_one]
State after:
no goals