Theorem: primesOver_eq_empty_of_not_isPrime (FltRegular/NumberTheory/GaloisPrime.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
⊢ primesOver S p = ∅
Tactic:
rw [← Set.not_nonempty_iff_eq_empty]
State after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
⊢ ¬(primesOver S p).Nonempty

State before:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
⊢ ¬(primesOver S p).Nonempty
Tactic:
rintro ⟨P, hP⟩
State after:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
P : Ideal S
hP : P ∈ primesOver S p
⊢ False

State before:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
hp : ¬p.IsPrime
P : Ideal S
hP : P ∈ primesOver S p
⊢ False
Tactic:
exact hp (hP.2 ▸ hP.1.comap _)
State after:
no goals