Theorem: isUnramifiedAt_iff_normalizedFactors_nodup (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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔ (normalizedFactors (Ideal.map (algebraMap R S) p)).Nodup
Tactic:
simp_rw [Multiset.nodup_iff_count_eq_one, ← Multiset.mem_toFinset,
  ← factors_eq_normalizedFactors]
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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔
    ∀ a ∈ (factors (Ideal.map (algebraMap R S) p)).toFinset,
      Multiset.count a (factors (Ideal.map (algebraMap R S) p)) = 1

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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔
    ∀ a ∈ (factors (Ideal.map (algebraMap R S) p)).toFinset,
      Multiset.count a (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
show _ ↔ ∀ P ∈ (primesOverFinset S p : Set (Ideal S)), _
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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔ ∀ P ∈ ↑(primesOverFinset S p), Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1

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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔ ∀ P ∈ ↑(primesOverFinset S p), Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
simp_rw [IsUnramifiedAt, coe_primesOverFinset S 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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ (∀ P ∈ primesOver S p, Ideal.ramificationIdx (algebraMap R S) p P = 1) ↔
    ∀ P ∈ primesOver S p, Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1

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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
⊢ (∀ P ∈ primesOver S p, Ideal.ramificationIdx (algebraMap R S) p P = 1) ↔
    ∀ P ∈ primesOver S p, Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
refine forall₂_congr (fun 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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1 ↔ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1

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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.ramificationIdx (algebraMap R S) p P = 1 ↔ Multiset.count P (factors (Ideal.map (algebraMap R S) p)) = 1
Tactic:
rw [Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count]
State after:
case hp0
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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.map (algebraMap R S) p ≠ ⊥

case hP
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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ P.IsPrime

case hP0
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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ P ≠ ⊥

State before:
case hp0
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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ Ideal.map (algebraMap R S) p ≠ ⊥
Tactic:
exact (Ideal.map_eq_bot_iff_of_injective
  (NoZeroSMulDivisors.algebraMap_injective R S)).not.mpr hp
State after:
no goals

State before:
case hP
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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ P.IsPrime
Tactic:
exact hP.1
State after:
no goals

State before:
case hP0
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✝² : NoZeroSMulDivisors R S
inst✝¹ : IsDedekindDomain S
p : Ideal R
inst✝ : p.IsPrime
hp : p ≠ ⊥
P : Ideal S
hP : P ∈ primesOver S p
⊢ P ≠ ⊥
Tactic:
exact ne_bot_of_mem_primesOver hp hP
State after:
no goals