-- 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:
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
⊢ map (algebraMap R S) p ≠ ⊥

Tactic:
rwa [Ne, Ideal.map_eq_bot_iff_le_ker, (RingHom.injective_iff_ker_eq_bot _).mp <|
  algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff]

Result:
no goals

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
⊢ ∑ x ∈ (factors (map (algebraMap R S) p)).toFinset.attach, e ↑x * f ↑x =
    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach, finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)

Tactic:
refine Finset.sum_congr rfl fun P _ => ?_

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 : { 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)

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

Tactic:
exact finrank_quotient_map p K L

Result:
no goals

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 ∈ (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)

Tactic:
rw [← Finset.sum_attach]

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
⊢ ∑ x ∈ (factors (map (algebraMap R S) p)).toFinset.attach, e ↑x * f ↑x =
    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach, finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)

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 ≠ ⊥
⊢ ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, ramificationIdx (algebraMap R S) p P * p.inertiaDeg P = finrank K L

Tactic:
set e := ramificationIdx (algebraMap R S) p

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
⊢ ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * p.inertiaDeg P = finrank K L

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

Tactic:
refine LinearEquiv.finrank_eq (Factors.piQuotientLinearEquiv S p ?_).symm

Result:
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
⊢ map (algebraMap R S) p ≠ ⊥