-- 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
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
⊢ map g I ≠ 0

Tactic:
by_contra h

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
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
h : map g I = 0
⊢ False

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
⊢ 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 hcp : ⊤ = map g P ⊔ map g I := by rw [← map_sup, hcp, map_top g]

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
⊢ 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 ≠ ⊥
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
⊢ ⊤ = map g P ⊔ map g I

Tactic:
rw [← map_sup, hcp, map_top g]

Result:
no goals