Theorem: prod_smul_primesOver (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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn S p
Tactic:
have : IsDomain S :=
  (IsIntegralClosure.equiv R S L (integralClosure R L)).toMulEquiv.isDomain (integralClosure R 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this : IsDomain S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this : IsDomain S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn S p
Tactic:
have := IsIntegralClosure.isDedekindDomain R K L 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn S p
Tactic:
have := IsIntegralClosure.isNoetherian R K L 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : p = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn S p
Tactic:
rw [← prod_primesOverFinset_pow_ramificationIdxIn K L p hp]
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = ((∏ P ∈ primesOverFinset S p, P) ^ Ideal.ramificationIdxIn S p) ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = ((∏ P ∈ primesOverFinset S p, P) ^ Ideal.ramificationIdxIn S p) ^ Ideal.inertiaDegIn S p
Tactic:
delta Finset.prod
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val).prod =
    ((Multiset.map (fun P => P) (primesOverFinset S p).val).prod ^ Ideal.ramificationIdxIn S p) ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val).prod =
    ((Multiset.map (fun P => P) (primesOverFinset S p).val).prod ^ Ideal.ramificationIdxIn S p) ^ Ideal.inertiaDegIn S p
Tactic:
rw [← pow_mul, ← Multiset.prod_nsmul, Multiset.map_id']
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val).prod =
    ((Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val).prod

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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val).prod =
    ((Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val).prod
Tactic:
congr
State after:
case neg.e_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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val =
    (Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val

State before:
case neg.e_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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
⊢ Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val =
    (Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val
Tactic:
ext P'
State after:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Multiset.count P' ((Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val)

State before:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Multiset.count P' ((Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p) • (primesOverFinset S p).val)
Tactic:
rw [Multiset.count_nsmul, primesOverFinset, Multiset.toFinset_val, Multiset.count_dedup]
State after:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ factors (Ideal.map (algebraMap R S) p) then 1 else 0

State before:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ factors (Ideal.map (algebraMap R S) p) then 1 else 0
Tactic:
simp_rw [← Multiset.mem_toFinset, ← Finset.mem_coe]
State after:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p *
      if P' ∈ ↑(factors (Ideal.map (algebraMap R S) p)).toFinset then 1 else 0

State before:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p *
      if P' ∈ ↑(factors (Ideal.map (algebraMap R S) p)).toFinset then 1 else 0
Tactic:
rw [← primesOverFinset]
State after:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ ↑(primesOverFinset S p) then 1 else 0

State before:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ ↑(primesOverFinset S p) then 1 else 0
Tactic:
simp_rw [coe_primesOverFinset S p hp]
State after:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0

State before:
case neg.e_a.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0
Tactic:
by_cases hP' : P' ∈ primesOver 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0

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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0

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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝ : IsDomain S
this : IsDedekindDomain S
⊢ 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : p = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) p ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥
Tactic:
have := P.prop
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
this : ↑P ∈ primesOver S ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
this : ↑P ∈ primesOver S ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥
Tactic:
have hRS : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
this : ↑P ∈ primesOver S ⊥
hRS : Algebra.IsIntegral R S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
this : ↑P ∈ primesOver S ⊥
hRS : Algebra.IsIntegral R S
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥
Tactic:
simp_rw [primesOver_bot (S := S),
  Set.mem_singleton_iff] at this
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn 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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ ∏ σ : L ≃ₐ[K] L, ↑(σ • P) = Ideal.map (algebraMap R S) ⊥ ^ Ideal.inertiaDegIn S ⊥
Tactic:
simp_rw [coe_smul_primesOver, this,
  Ideal.comap_bot_of_injective _ (galRestrict R K L S _).injective, Finset.prod_const,
  Ideal.map_bot, Ideal.inertiaDegIn_bot R S]
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ ⊥ ^ Finset.univ.card = ⊥ ^ finrank 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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ ⊥ ^ Finset.univ.card = ⊥ ^ finrank R S
Tactic:
refine (zero_pow ?_).trans (zero_pow ?_).symm
State after:
case pos.refine_1
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ Finset.univ.card ≠ 0

case pos.refine_2
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ finrank R S ≠ 0

State before:
case pos.refine_1
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ Finset.univ.card ≠ 0
Tactic:
rw [Finset.card_univ, Ne, Fintype.card_eq_zero_iff]
State after:
case pos.refine_1
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ ¬IsEmpty (L ≃ₐ[K] L)

State before:
case pos.refine_1
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ ¬IsEmpty (L ≃ₐ[K] L)
Tactic:
simp only [not_isEmpty_of_nonempty, not_false_eq_true]
State after:
no goals

State before:
case pos.refine_2
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
⊢ finrank R S ≠ 0
Tactic:
have hR := not_imp_not.mp (Ring.ne_bot_of_isMaximal_of_not_isField ‹_›) rfl
State after:
case pos.refine_2
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
hR : IsField R
⊢ finrank R S ≠ 0

State before:
case pos.refine_2
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✝¹ : IsGalois K L
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this : ↑P = ⊥
hR : IsField R
⊢ finrank R S ≠ 0
Tactic:
letI : Field R := hR.toField
State after:
case pos.refine_2
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✝¹ : IsGalois K L
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this✝ : ↑P = ⊥
hR : IsField R
this : Field R := hR.toField
⊢ finrank R S ≠ 0

State before:
case pos.refine_2
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✝¹ : IsGalois K L
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS✝ : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
P : ↑(primesOver S ⊥)
inst✝ : ⊥.IsMaximal
hRS : Algebra.IsIntegral R S
this✝ : ↑P = ⊥
hR : IsField R
this : Field R := hR.toField
⊢ finrank R S ≠ 0
Tactic:
exact finrank_pos.ne'
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0
Tactic:
rw [if_pos hP', mul_one, Multiset.count_map]
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
⊢ Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
⊢ Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p
Tactic:
have : Fintype (primesOver S p) := (primesOver_finite S p hp).fintype
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p
Tactic:
apply mul_left_injective₀ (Set.ncard_ne_zero_of_mem P.prop)
State after:
case pos.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ (fun a => a * (primesOver S p).ncard) (Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val)) =
    (fun a => a * (primesOver S p).ncard) (Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p)

State before:
case pos.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ (fun a => a * (primesOver S p).ncard) (Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val)) =
    (fun a => a * (primesOver S p).ncard) (Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p)
Tactic:
dsimp only
State after:
case pos.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) * (primesOver S p).ncard =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * (primesOver S p).ncard

State before:
case pos.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) * (primesOver S p).ncard =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * (primesOver S p).ncard
Tactic:
rw [Ideal.ramificationIdxIn_mul_inertiaDegIn_mul_ncard_primesOver K L p hp,
  ← IsGalois.card_aut_eq_finrank, ← MulAction.card_orbit_mul_card_stabilizer_eq_card_group
    (L ≃ₐ[K] L) P, MulAction.orbit_eq_univ, mul_comm]
State after:
case pos.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ (primesOver S p).ncard * Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Fintype.card ↑Set.univ * Fintype.card ↥(MulAction.stabilizer (L ≃ₐ[K] L) P)

State before:
case pos.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ (primesOver S p).ncard * Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Fintype.card ↑Set.univ * Fintype.card ↥(MulAction.stabilizer (L ≃ₐ[K] L) P)
Tactic:
simp only [Fintype.card_ofFinset, Set.mem_univ, Finset.mem_univ, forall_true_left,
  Subtype.forall, implies_true, forall_const, Finset.filter_true_of_mem,
  MulAction.mem_stabilizer_iff, Finset.card_univ, ← Set.Nat.card_coe_set_eq,
  Nat.card_eq_fintype_card]
State after:
case pos.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Fintype.card ↑(primesOver S p) * Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Fintype.card ↑(primesOver S p) * Fintype.card { x // x • P = P }

State before:
case pos.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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Fintype.card ↑(primesOver S p) * Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) =
    Fintype.card ↑(primesOver S p) * Fintype.card { x // x • P = P }
Tactic:
congr 1
State after:
case pos.a.e_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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) = Fintype.card { x // x • P = P }

State before:
case pos.a.e_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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Multiset.card (Multiset.filter (fun a => P' = ↑(a • P)) Finset.univ.val) = Fintype.card { x // x • P = P }
Tactic:
rw [← Finset.filter_val, ← Finset.card, ← Fintype.card_subtype]
State after:
case pos.a.e_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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }

State before:
case pos.a.e_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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }
Tactic:
obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq (L ≃ₐ[K] L) P ⟨P', hP'⟩
State after:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }

State before:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }
Tactic:
have : P' = ↑(σ • P) := by rw [hσ]
State after:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this✝ : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
this : P' = ↑(σ • P)
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }

State before:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this✝ : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
this : P' = ↑(σ • P)
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }
Tactic:
simp_rw [this, ← Subtype.ext_iff, ← eq_inv_smul_iff (a := σ), ← mul_smul, eq_comm (a := P)]
State after:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this✝ : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
this : P' = ↑(σ • P)
⊢ Fintype.card { x // (σ⁻¹ * x) • P = P } = Fintype.card { x // x • P = P }

State before:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this✝ : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
this : P' = ↑(σ • P)
⊢ Fintype.card { x // (σ⁻¹ * x) • P = P } = Fintype.card { x // x • P = P }
Tactic:
exact Fintype.card_congr
  { toFun := fun x ↦ ⟨σ⁻¹ * x, x.prop⟩,
    invFun := fun x ↦ ⟨σ * x, (inv_mul_cancel_left σ x).symm ▸ x.prop⟩,
    left_inv := fun x ↦ Subtype.ext (mul_inv_cancel_left σ x),
    right_inv := fun x ↦ Subtype.ext (inv_mul_cancel_left σ x) }
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
⊢ P' = ↑(σ • P)
Tactic:
rw [hσ]
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0
Tactic:
rw [if_neg hP', mul_zero, Multiset.count_eq_zero]
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ P' ∉ Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val

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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ P' ∉ Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val
Tactic:
simp only [Multiset.mem_map, Finset.mem_val, Finset.mem_univ, true_and, not_exists]
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ ∀ (x : L ≃ₐ[K] L), ¬↑(x • P) = 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ ∀ (x : L ≃ₐ[K] L), ¬↑(x • P) = P'
Tactic:
rintro σ rfl
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
σ : L ≃ₐ[K] L
hP' : ↑(σ • P) ∉ primesOver S p
⊢ False

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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
σ : L ≃ₐ[K] L
hP' : ↑(σ • P) ∉ primesOver S p
⊢ False
Tactic:
exact hP' (σ • P).2
State after:
no goals