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

State before:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
⊢ ↑(primesOverFinset S p) = primesOver S p
Tactic:
classical
ext P
have : p.map (algebraMap R S) ≠ ⊥ := by
  rwa [Ne, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective R S)]
simp only [Finset.mem_coe, Multiset.mem_toFinset, Ideal.mem_normalizedFactors_iff this,
  factors_eq_normalizedFactors, Ideal.map_le_iff_le_comap, primesOverFinset]
exact ⟨fun H ↦ ⟨H.1, ((hp'.isMaximal hp).eq_of_le (H.1.comap _).ne_top H.2).symm⟩,
  fun H ↦ ⟨H.1, H.2.ge⟩⟩
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
⊢ ↑(primesOverFinset S p) = primesOver S p
Tactic:
ext P
State after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
⊢ P ∈ ↑(primesOverFinset S p) ↔ P ∈ primesOver S p

State before:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
⊢ P ∈ ↑(primesOverFinset S p) ↔ P ∈ primesOver S p
Tactic:
have : p.map (algebraMap R S) ≠ ⊥ := by
  rwa [Ne, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective R S)]
State after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
this : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ P ∈ ↑(primesOverFinset S p) ↔ P ∈ primesOver S p

State before:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
this : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ P ∈ ↑(primesOverFinset S p) ↔ P ∈ primesOver S p
Tactic:
simp only [Finset.mem_coe, Multiset.mem_toFinset, Ideal.mem_normalizedFactors_iff this,
  factors_eq_normalizedFactors, Ideal.map_le_iff_le_comap, primesOverFinset]
State after:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
this : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ P.IsPrime ∧ p ≤ Ideal.comap (algebraMap R S) P ↔ P ∈ primesOver S p

State before:
case h
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
this : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ P.IsPrime ∧ p ≤ Ideal.comap (algebraMap R S) P ↔ P ∈ primesOver S p
Tactic:
exact ⟨fun H ↦ ⟨H.1, ((hp'.isMaximal hp).eq_of_le (H.1.comap _).ne_top H.2).symm⟩,
  fun H ↦ ⟨H.1, H.2.ge⟩⟩
State after:
no goals

State before:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Ring.DimensionLEOne R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
p : Ideal R
hp : p ≠ ⊥
hp' : p.IsPrime
P : Ideal S
⊢ Ideal.map (algebraMap R S) p ≠ ⊥
Tactic:
rwa [Ne, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective R S)]
State after:
no goals