-- Mathlib/NumberTheory/RamificationInertia/Galois.lean
theorem ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn [IsGalois K L] :
    (primesOver p B).ncard * (ramificationIdxIn p B * inertiaDegIn p B) = Module.finrank K L

Proof state:
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
this : FaithfulSMul A B
⊢ ∑ _x ∈ primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B =
    ∑ P ∈ (UniqueFactorizationMonoid.factors (map (algebraMap A B) p)).toFinset,
      ramificationIdx (algebraMap A B) p P * p.inertiaDeg P

Tactic:
apply Finset.sum_congr rfl

Result:
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
this : FaithfulSMul A B
⊢ ∀ x ∈ primesOverFinset p B,
    p.ramificationIdxIn B * p.inertiaDegIn B = ramificationIdx (algebraMap A B) p x * p.inertiaDeg x

Proof state:
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
⊢ (p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B) = Module.finrank K L

Tactic:
have : FaithfulSMul A B := FaithfulSMul.of_field_isFractionRing A B K L

Result:
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
this : FaithfulSMul A B
⊢ (p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B) = Module.finrank K L

Proof state:
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
this : FaithfulSMul A B
⊢ ∑ _x ∈ primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B = Module.finrank K L

Tactic:
rw [← sum_ramification_inertia B p K L hpb]

Result:
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
this : FaithfulSMul A B
⊢ ∑ _x ∈ primesOverFinset p B, p.ramificationIdxIn B * p.inertiaDegIn B =
    ∑ P ∈ (UniqueFactorizationMonoid.factors (map (algebraMap A B) p)).toFinset,
      ramificationIdx (algebraMap A B) p P * p.inertiaDeg P

Proof state:
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
this : FaithfulSMul A B
P : Ideal B
hp : P ∈ p.primesOver B
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = ramificationIdx (algebraMap A B) p P * p.inertiaDeg P

Tactic:
obtain ⟨_, _⟩ := hp

Result:
case intro
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
this : FaithfulSMul A B
P : Ideal B
left✝ : P.IsPrime
right✝ : P.LiesOver p
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = ramificationIdx (algebraMap A B) p P * p.inertiaDeg P

Proof state:
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
this : FaithfulSMul A B
⊢ ∀ x ∈ primesOverFinset p B,
    p.ramificationIdxIn B * p.inertiaDegIn B = ramificationIdx (algebraMap A B) p x * p.inertiaDeg x

Tactic:
intro P hp

Result:
A : Type u_1
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDedekindDomain A
p : Ideal A
hpb : p ≠ ⊥
inst✝¹⁶ : p.IsMaximal
B : Type u_2
inst✝¹⁵ : CommRing B
inst✝¹⁴ : IsDedekindDomain B
inst✝¹³ : Algebra A B
inst✝¹² : Module.Finite A B
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra A K
inst✝⁸ : IsFractionRing A K
inst✝⁷ : Algebra B L
inst✝⁶ : IsFractionRing B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
this : FaithfulSMul A B
P : Ideal B
hp : P ∈ primesOverFinset p B
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = ramificationIdx (algebraMap A B) p P * p.inertiaDeg P