-- 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
P : Ideal B
hp : P ∈ primesOverFinset p B
⊢ p.ramificationIdxIn B * p.inertiaDegIn B = ramificationIdx (algebraMap A B) p P * p.inertiaDeg P

Tactic:
rw [← Finset.mem_coe, coe_primesOverFinset hpb B] at 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 ∈ p.primesOver B
⊢ 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
⊢ (p.primesOver B).ncard * (p.ramificationIdxIn B * p.inertiaDegIn B) = Module.finrank K L

Tactic:
rw [← smul_eq_mul, ← coe_primesOverFinset hpb B, Set.ncard_coe_Finset, ← Finset.sum_const]

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 = Module.finrank K L

Proof state:
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

Tactic:
rw [ramificationIdxIn_eq_ramificationIdx p P K L, inertiaDegIn_eq_inertiaDeg p P K L]

Result:
no goals