Theorem: ideal_neq_top (Kaplanski4/Kaplanski.lean)

State before:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : P ∈ Kaplansky.set S
⊢ P ≠ ⊤
Tactic:
intro h
State after:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : P ∈ Kaplansky.set S
h : P = ⊤
⊢ False

State before:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : P ∈ Kaplansky.set S
h : P = ⊤
⊢ False
Tactic:
rw [Kaplansky.set, h, Set.mem_setOf, Set.eq_empty_iff_forall_not_mem] at hP
State after:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False

State before:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : Set.Nonempty ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False
Tactic:
rw [Set.nonempty_def] at hS
State after:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : ∃ x, x ∈ ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False

State before:
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : ∃ x, x ∈ ↑S
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
⊢ False
Tactic:
cases' hS with x h₂
State after:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
x : R
h₂ : x ∈ ↑S
⊢ False

State before:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
hP : ∀ (x : R), x ∉ ↑⊤ ∩ ↑S
h : P = ⊤
x : R
h₂ : x ∈ ↑S
⊢ False
Tactic:
specialize hP x
State after:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
h : P = ⊤
x : R
h₂ : x ∈ ↑S
hP : x ∉ ↑⊤ ∩ ↑S
⊢ False

State before:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
h : P = ⊤
x : R
h₂ : x ∈ ↑S
hP : x ∉ ↑⊤ ∩ ↑S
⊢ False
Tactic:
apply hP
State after:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
h : P = ⊤
x : R
h₂ : x ∈ ↑S
hP : x ∉ ↑⊤ ∩ ↑S
⊢ x ∈ ↑⊤ ∩ ↑S

State before:
case intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
P : Ideal R
h : P = ⊤
x : R
h₂ : x ∈ ↑S
hP : x ∉ ↑⊤ ∩ ↑S
⊢ x ∈ ↑⊤ ∩ ↑S
Tactic:
exact (Set.mem_inter (Set.mem_univ x) h₂)
State after:
no goals