-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem sum_ramification_inertia (K L : Type*) [Field K] [Field L] [IsDedekindDomain R]
    [Algebra R K] [IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L]
    [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] [Module.Finite R S]
    [p.IsMaximal] (hp0 : p ≠ ⊥) :
    (∑ P ∈ (factors (map (algebraMap R S) p)).toFinset,
        ramificationIdx (algebraMap R S) p P * inertiaDeg p P) =
      finrank K L

Proof state:
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : IsDedekindDomain S
inst✝¹³ : Algebra R S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p
⊢ ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * p.inertiaDeg P = finrank K L

Tactic:
set f := inertiaDeg p (S := S)

Result:
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : IsDedekindDomain S
inst✝¹³ : Algebra R S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p
f : Ideal S → [inst : Algebra R S] → ℕ := p.inertiaDeg
⊢ ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * f P = finrank K L

Proof state:
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : IsDedekindDomain S
inst✝¹³ : Algebra R S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p
f : Ideal S → [inst : Algebra R S] → ℕ := p.inertiaDeg
⊢ ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * f P = finrank K L

Tactic:
calc
  (∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * f P) =
      ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach,
        finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ e P) := ?_
  _ = finrank (R ⧸ p)
        (∀ P : (factors (map (algebraMap R S) p)).toFinset, S ⧸ (P : Ideal S) ^ e P) :=
    (finrank_pi_fintype (R ⧸ p)).symm
  _ = finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) := ?_
  _ = finrank K L := ?_

Result:
case calc_1
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : IsDedekindDomain S
inst✝¹³ : Algebra R S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p
f : Ideal S → [inst : Algebra R S] → ℕ := p.inertiaDeg
⊢ ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * f P =
    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach, finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)

case calc_2
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : IsDedekindDomain S
inst✝¹³ : Algebra R S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p
f : Ideal S → [inst : Algebra R S] → ℕ := p.inertiaDeg
⊢ finrank (R ⧸ p) ((P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }) → S ⧸ ↑P ^ e ↑P) =
    finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p)

case calc_3
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : IsDedekindDomain S
inst✝¹³ : Algebra R S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p
f : Ideal S → [inst : Algebra R S] → ℕ := p.inertiaDeg
⊢ finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) = finrank K L

Proof state:
case calc_1
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
p : Ideal R
inst✝¹⁴ : IsDedekindDomain S
inst✝¹³ : Algebra R S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := ramificationIdx (algebraMap R S) p
f : Ideal S → [inst : Algebra R S] → ℕ := p.inertiaDeg
P : { x // x ∈ (factors (map (algebraMap R S) p)).toFinset }
x✝ : P ∈ (factors (map (algebraMap R S) p)).toFinset.attach
⊢ e ↑P * f ↑P = finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)

Tactic:
rw [Factors.finrank_pow_ramificationIdx]

Result:
no goals