-- 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
⊢ ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

Tactic:
have hf0 : map f p ≠ ⊥ :=
  ne_bot_of_map_ne_bot (Eq.mp (congrArg (fun I ↦ I ≠ ⊥) (map_map f g).symm) hfg)

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 ≠ ⊥
⊢ 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 ≠ ⊥
⊢ ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

Tactic:
have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0

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 ≠ ⊥
⊢ 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
hntq : ¬⊤ ≤ Q
h : map g I = 0
hcp : ⊤ = map g P
⊢ False

Tactic:
exact hntq (hcp.trans_le hg)

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 ≠ ⊥
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

Tactic:
simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp

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
hntq : ¬⊤ ≤ Q
h : map g I = 0
hcp : ⊤ = map g P
⊢ False

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
⊢ ramificationIdx (g.comp f) p Q = ramificationIdx f p P * ramificationIdx g P Q

Tactic:
classical
have hf0 : map f p ≠ ⊥ :=
  ne_bot_of_map_ne_bot (Eq.mp (congrArg (fun I ↦ I ≠ ⊥) (map_map f g).symm) hfg)
have hp0 : P ≠ ⊥ := ne_bot_of_map_ne_bot hg0
have hq0 : Q ≠ ⊥ := ne_bot_of_le_ne_bot hg0 hg
letI : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hp0 hpm
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]
rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩
have hcp : ⊤ = map g P ⊔ map g I := by rw [← map_sup, hcp, map_top g]
have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
nth_rw 1 [heq, map_mul, Ideal.map_pow, normalizedFactors_mul (pow_ne_zero _ hg0) <| by
  by_contra h
  simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp
  exact hntq (hcp.trans_le hg), Multiset.count_add, normalizedFactors_pow, Multiset.count_nsmul]
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:
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))

Tactic:
nth_rw 1 [heq, map_mul, Ideal.map_pow, normalizedFactors_mul (pow_ne_zero _ hg0) <| by
  by_contra h
  simp only [h, Submodule.zero_eq_bot, bot_le, sup_of_le_left] at hcp
  exact hntq (hcp.trans_le hg), Multiset.count_add, normalizedFactors_pow, Multiset.count_nsmul]

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