-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_tower [IsDedekindDomain S] [IsDedekindDomain T] {f : R →+* S} {g : S →+* T}
    {p : Ideal R} {P : Ideal S} {Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime]
    (hg0 : map g P ≠ ⊥) (hfg : map (g.comp f) p ≠ ⊥) (hg : map g P ≤ Q) :
    ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
⊢ Multiset.count Q (normalizedFactors (map g (map f p))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map g P))

Tactic:
rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩

Result:
case intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
⊢ Multiset.count Q (normalizedFactors (map g (map f p))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map g P))

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
⊢ ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

Tactic:
have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
⊢ ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
⊢ ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

Tactic:
rw [IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hf0 hpm hp0,
  IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hg0 hqm hq0,
  IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hfg hqm hq0, ← map_map]

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
⊢ Multiset.count Q (normalizedFactors (map g (map f p))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map g P))

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map g P ⊔ map g I
hntq : ¬⊤ ≤ Q
⊢ Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map g P)) +
      Multiset.count Q (normalizedFactors (map g I)) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map g P))

Tactic:
exact add_right_eq_self.mpr <| Decidable.byContradiction fun h ↦ hntq <| hcp.trans_le <|
  sup_le hg <| le_of_dvd <| dvd_of_mem_normalizedFactors <| Multiset.count_ne_zero.mp h

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
⊢ ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

Tactic:
letI : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
⊢ ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

Proof state:
case intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map g P ⊔ map g I
⊢ Multiset.count Q (normalizedFactors (map g (map f p))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map g P))

Tactic:
have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))

Result:
case intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
f : R →+* S
g : S →+* T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map g P ≠ ⊥
hfg : map (g.comp f) p ≠ ⊥
hg : map g P ≤ Q
hf0 : map f p ≠ ⊥
hp0 : P ≠ ⊥
hq0 : Q ≠ ⊥
this : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
I : Ideal S
hcp✝ : P ⊔ I = ⊤
heq : map f p = P ^ Multiset.count P (normalizedFactors (map f p)) * I
hcp : ⊤ = map g P ⊔ map g I
hntq : ¬⊤ ≤ Q
⊢ Multiset.count Q (normalizedFactors (map g (map f p))) =
    Multiset.count P (normalizedFactors (map f p)) * Multiset.count Q (normalizedFactors (map g P))