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

State before:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
⊢ (primesOver S p).Nonempty
Tactic:
have := Ideal.bot_prime (α := S)
State after:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ (primesOver S p).Nonempty

State before:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ (primesOver S p).Nonempty
Tactic:
obtain ⟨Q, _, hQ⟩ := Ideal.exists_ideal_over_prime_of_isIntegral p ⊥
  (by rw [Ideal.comap_bot_of_injective _
    (NoZeroSMulDivisors.algebraMap_injective R S)]; exact bot_le)
State after:
case intro.intro
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
Q : Ideal S
left✝ : Q ≥ ⊥
hQ : Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = p
⊢ (primesOver S p).Nonempty

State before:
case intro.intro
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
Q : Ideal S
left✝ : Q ≥ ⊥
hQ : Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = p
⊢ (primesOver S p).Nonempty
Tactic:
exact ⟨Q, hQ⟩
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ Ideal.comap (algebraMap R ?m.22477) ⊥ ≤ p
Tactic:
rw [Ideal.comap_bot_of_injective _
(NoZeroSMulDivisors.algebraMap_injective R S)]
State after:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ ⊥ ≤ p

State before:
R : Type u_2
S : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain S
inst✝² : NoZeroSMulDivisors R S
inst✝¹ : Algebra.IsIntegral R S
p : Ideal R
inst✝ : p.IsPrime
this : ⊥.IsPrime
⊢ ⊥ ≤ p
Tactic:
exact bot_le
State after:
no goals