case he
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ ramificationIdx (algebraMap R S) p ↑P ≠ 0

case hP0
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ ↑P ≠ ⊥

case he
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ ramificationIdx (algebraMap R S) p ↑P ≠ 0
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ finrank (R ⧸ p) (S ⧸ ↑P ^ ramificationIdx (algebraMap R S) p ↑P) =
    ramificationIdx (algebraMap R S) p ↑P * inertiaDeg (algebraMap R S) p ↑P
rw [finrank_prime_pow_ramificationIdx, inertiaDeg_algebraMap]
no goals
case he
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ ramificationIdx (algebraMap R S) p ↑P ≠ 0

case hP0
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ ↑P ≠ ⊥

case he
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P✝ : Ideal S
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra R S
inst✝ : IsMaximal p
P : { x // x ∈ Multiset.toFinset (factors (map (algebraMap R S) p)) }
⊢ ramificationIdx (algebraMap R S) p ↑P ≠ 0
exacts [NeZero.ne _, Factors.ne_bot p P]