Theorem: prod_primesOverFinset_of_isUnramified (FltRegular/NumberTheory/Unramified.lean)

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P = Ideal.map (algebraMap R S) p
Tactic:
classical
have hpbot' : p.map (algebraMap R S) ≠ ⊥ := (Ideal.map_eq_bot_iff_of_injective
  (NoZeroSMulDivisors.iff_algebraMap_injective.mp ‹_›)).not.mpr hp
rw [← associated_iff_eq.mp (factors_pow_count_prod hpbot')]
apply Finset.prod_congr rfl
intros P hP
convert (pow_one _).symm
rw [← Finset.mem_coe, coe_primesOverFinset S p hp] at hP
rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count hpbot' hP.1
  (ne_bot_of_mem_primesOver hp hP)]
exact IsUnramified.isUnramifiedAt _ hp _ hP
State after:
no goals

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P = Ideal.map (algebraMap R S) p
Tactic:
have hpbot' : p.map (algebraMap R S) ≠ ⊥ := (Ideal.map_eq_bot_iff_of_injective
  (NoZeroSMulDivisors.iff_algebraMap_injective.mp ‹_›)).not.mpr hp
State after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P = Ideal.map (algebraMap R S) p

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P = Ideal.map (algebraMap R S) p
Tactic:
rw [← associated_iff_eq.mp (factors_pow_count_prod hpbot')]
State after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P =
    ∏ p_1 ∈ (factors (Ideal.map (algebraMap R S) p)).toFinset,
      p_1 ^ Multiset.count p_1 (factors (Ideal.map (algebraMap R S) p))

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∏ P ∈ primesOverFinset S p, P =
    ∏ p_1 ∈ (factors (Ideal.map (algebraMap R S) p)).toFinset,
      p_1 ^ Multiset.count p_1 (factors (Ideal.map (algebraMap R S) p))
Tactic:
apply Finset.prod_congr rfl
State after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∀ x ∈ primesOverFinset S p, x = x ^ Multiset.count x (factors (Ideal.map (algebraMap R S) p))

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
⊢ ∀ x ∈ primesOverFinset S p, x = x ^ Multiset.count x (factors (Ideal.map (algebraMap R S) p))
Tactic:
intros P hP
State after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ P = P ^ Multiset.count P (factors (Ideal.map (algebraMap R S) p))

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ P = P ^ Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Tactic:
convert (pow_one _).symm
State after:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1

State before:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
rw [← Finset.mem_coe, coe_primesOverFinset S p hp] at hP
State after:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1

State before:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count hpbot' hP.1
  (ne_bot_of_mem_primesOver hp hP)]
State after:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1

State before:
case h.e'_3.h.e'_6
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsUnramified R S
inst✝² : IsDedekindDomain S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1
Tactic:
exact IsUnramified.isUnramifiedAt _ hp _ hP
State after:
no goals