P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
this : p ∈ univ
⊢ False
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
⊢ False
have := mem_univ p
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
this : p ∈ ↑I
⊢ False
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
this : p ∈ univ
⊢ False
rw [← hp] at this
no goals
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
this : p ∈ ↑I
⊢ False
exact nmem this