Theorem: ramificationIdxIn_smul_primesOverFinset (FltRegular/NumberTheory/GaloisPrime.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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Tactic:
have hRS : Function.Injective (algebraMap R S) := by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : Function.Injective ⇑(algebraMap R S)
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = 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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : Function.Injective ⇑(algebraMap R S)
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Tactic:
rw [← NoZeroSMulDivisors.iff_algebraMap_injective] at hRS
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = 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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Tactic:
by_cases hp : p = ⊥
State after:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : p = ⊥
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)

case neg
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)

State before:
case neg
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Tactic:
ext P
State after:
case neg.a
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))

State before:
case neg.a
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Tactic:
by_cases hP : P ∈ primesOverFinset S p
State after:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))

case neg
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∉ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))

State before:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))

case neg
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∉ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Tactic:
swap
State after:
case neg
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∉ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))

case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))

State before:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Tactic:
have hP' := hP
State after:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP hP' : P ∈ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))

State before:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP hP' : P ∈ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Tactic:
rw [primesOverFinset, Multiset.mem_toFinset] at hP
State after:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ factors (Ideal.map (algebraMap R S) p)
hP' : P ∈ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))

State before:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ factors (Ideal.map (algebraMap R S) p)
hP' : P ∈ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Tactic:
rw [← Finset.mem_coe, coe_primesOverFinset S p hp] at hP'
State after:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ factors (Ideal.map (algebraMap R S) p)
hP' : P ∈ primesOver S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))

State before:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ factors (Ideal.map (algebraMap R S) p)
hP' : P ∈ primesOver S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Tactic:
rw [Ideal.ramificationIdxIn_eq_ramificationIdx K L p P hP', Multiset.count_nsmul,
  Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count _ hP'.1
  (ne_bot_of_mem_primesOver hp hP'), primesOverFinset,
  Multiset.toFinset_val, Multiset.count_dedup, if_pos hP, mul_one]
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ factors (Ideal.map (algebraMap R S) p)
hP' : P ∈ primesOver S 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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∈ factors (Ideal.map (algebraMap R S) p)
hP' : P ∈ primesOver S p
⊢ Ideal.map (algebraMap R S) p ≠ ⊥
Tactic:
rwa [Ne, Ideal.map_eq_bot_iff_of_injective (NoZeroSMulDivisors.algebraMap_injective _ _)]
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
⊢ Function.Injective ⇑(algebraMap R S)
Tactic:
refine Function.Injective.of_comp (f := algebraMap S L) ?_
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))

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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
⊢ Function.Injective (⇑(algebraMap S L) ∘ ⇑(algebraMap R S))
Tactic:
rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))

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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap R K))
Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective _ _)
State after:
no goals

State before:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : p = ⊥
⊢ Ideal.ramificationIdxIn S p • (primesOverFinset S p).val = factors (Ideal.map (algebraMap R S) p)
Tactic:
subst hp
State after:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
hRS : NoZeroSMulDivisors R S
inst✝ : ⊥.IsPrime
⊢ Ideal.ramificationIdxIn S ⊥ • (primesOverFinset S ⊥).val = factors (Ideal.map (algebraMap R S) ⊥)

State before:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
hRS : NoZeroSMulDivisors R S
inst✝ : ⊥.IsPrime
⊢ Ideal.ramificationIdxIn S ⊥ • (primesOverFinset S ⊥).val = factors (Ideal.map (algebraMap R S) ⊥)
Tactic:
rw [Ideal.ramificationIdxIn_bot, zero_smul, Ideal.map_bot]
State after:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
hRS : NoZeroSMulDivisors R S
inst✝ : ⊥.IsPrime
⊢ 0 = factors ⊥

State before:
case pos
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
hRS : NoZeroSMulDivisors R S
inst✝ : ⊥.IsPrime
⊢ 0 = factors ⊥
Tactic:
exact factors_zero.symm
State after:
no goals

State before:
case neg
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∉ primesOverFinset S p
⊢ Multiset.count P (Ideal.ramificationIdxIn S p • (primesOverFinset S p).val) =
    Multiset.count P (factors (Ideal.map (algebraMap R S) p))
Tactic:
rw [Multiset.count_nsmul, Multiset.count_eq_zero_of_not_mem hP, mul_zero,
  Multiset.count_eq_zero_of_not_mem]
State after:
case neg
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∉ primesOverFinset S p
⊢ P ∉ factors (Ideal.map (algebraMap R S) p)

State before:
case neg
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✝² : IsDedekindDomain S
inst✝¹ : IsGalois K L
p : Ideal R
inst✝ : p.IsPrime
hRS : NoZeroSMulDivisors R S
hp : ¬p = ⊥
P : Ideal S
hP : P ∉ primesOverFinset S p
⊢ P ∉ factors (Ideal.map (algebraMap R S) p)
Tactic:
rwa [primesOverFinset, Multiset.mem_toFinset] at hP
State after:
no goals