-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Ramification (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsDedekindDomain S
inst_8 : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : Ne.{u_3 + 1} (α := Ideal T) (map (F := S →+* T) (algebraMap S T) P) ⊥
hfg : Ne.{u_3 + 1} (α := Ideal T) (map (F := R →+* T) (algebraMap R T) p) ⊥
hg : map (F := S →+* T) (algebraMap S T) P ≤ Q
have : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have₁ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₂ : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥
have₃ have₄ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₅ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₆ have₇ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥) (hq0 : Q ≠ ⊥),
    p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have₈ :
  ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥) (hq0 : Q ≠ ⊥),
    Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
      Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
        Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
⊢ p.ramificationIdx Q = p.ramificationIdx P * P.ramificationIdx Q
have have₉ : ∀ (hf0 : Ne.{u_2 + 1} (α := Ideal S) (map (F := R →+* S) f p) ⊥) (hp0 : P ≠ ⊥) (hq0 : Q ≠ ⊥) (I : Ideal S)
  (hcp : P ⊔ I = ⊤)
  (heq : map (F := R →+* S) f p = P ^ Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) * I),
  Multiset.count Q (normalizedFactors (map (R := S) (F := S →+* T) (algebraMap S T) (map (F := R →+* S) f p))) =
    Multiset.count P (normalizedFactors (map (F := R →+* S) f p)) *
      Multiset.count Q (normalizedFactors (map (F := S →+* T) (algebraMap S T) P))
Tactic: classical
  have hf0 : map (algebraMap R S) p ≠ ⊥ := by
    rw [IsScalarTower.algebraMap_eq R S T, ← map_map] at hfg
    exact ne_bot_of_map_ne_bot 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,
    IsScalarTower.algebraMap_eq R S T, ← map_map]
  rcases eq_prime_pow_mul_coprime hf0 P with ⟨I, hcp, heq⟩
  have hcp : ⊤ = map (algebraMap S T) P ⊔ map (algebraMap S T) I := by rw [← map_sup, hcp, map_top]
  have hntq : ¬ ⊤ ≤ Q := fun ht ↦ IsPrime.ne_top hqm (Iff.mpr (eq_top_iff_one Q) (ht trivial))
  nth_rw 1 [heq, Ideal.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_eq_left.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