chore(NumberTheory/*): remove last ramificationIdx_eq_ramificationIdx' (#41196)

This PR removes the last occurrences of `ramificationIdx_eq_ramificationIdx'`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

@@ -126,9 +126,8 @@ theorem ramificationIdx_span_zeta_sub_one :
     ramificationIdx' (span {hζ.toInteger - 1}) ℤ = p ^ k * (p - 1) := by
   have h := isPrime_span_zeta_sub_one p k hζ
   have hp0 : 𝒑 ≠ ⊥ := by simpa using hp.out.ne_zero
-  rw [← ramificationIdx_eq_ramificationIdx' 𝒑 _ hp0,
-    ← Nat.totient_prime_pow_succ hp.out, ← finrank _ K,
-    IsDedekindDomain.ramificationIdx_eq_multiplicity _ h, map_eq_span_zeta_sub_one_pow p k hζ,
+  rw [← Nat.totient_prime_pow_succ hp.out, ← finrank _ K,
+    IsDedekindDomain.ramificationIdx'_eq_multiplicity 𝒑, map_eq_span_zeta_sub_one_pow p k hζ,
     multiplicity_pow_self (span_zeta_sub_one_ne_bot p k hζ) (isUnit_iff.not.mpr h.ne_top)]
   exact map_ne_bot_of_ne_bot hp0
 

Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

@@ -294,9 +294,7 @@ private lemma ramificationIdxIn_eq_and_inertiaDegIn_eq (hp : p ≠ ⊥) :
   · exact Nat.pos_of_ne_zero <| inertiaDegIn_ne_zero (stabilizer Gal(L/K) P)
   · rw [ramificationIdxIn_eq_ramificationIdx p P Gal(L/K),
       ramificationIdxIn_eq_ramificationIdx _ P (stabilizer Gal(L/K) P)]
-    rw [← ramificationIdx_eq_ramificationIdx' p _ hp,
-      ← ramificationIdx_eq_ramificationIdx' 𝓟D _ h𝓟]
-    exact IsDedekindDomain.ramificationIdx_le_ramificationIdx _ _ _ hp
+    exact 𝓟D.ramificationIdx'_above_le P
   · rw [inertiaDegIn_eq_inertiaDeg p P Gal(L/K),
       inertiaDegIn_eq_inertiaDeg _ P (stabilizer Gal(L/K) P)]
     rw [← inertiaDeg_eq_inertiaDeg' p, ← inertiaDeg_eq_inertiaDeg' 𝓟D]

Mathlib/RingTheory/RamificationInertia/Ramification.lean

@@ -201,6 +201,24 @@ theorem ramificationIdx'_tower [r.LiesOver q] [Module.Flat S T] :
     apply ramificationIdx'_tower'
   · rw [ramificationIdx'_of_not_isPrime r R hr, ramificationIdx'_of_not_isPrime r S hr, mul_zero]
 
+theorem ramificationIdx'_below_dvd [r.LiesOver q] [Module.Flat S T] :
+    q.ramificationIdx' R ∣ r.ramificationIdx' R := by
+  use r.ramificationIdx' S
+  rw [← ramificationIdx'_tower]
+
+theorem ramificationIdx'_above_dvd [r.LiesOver q] [Module.Flat S T] :
+    r.ramificationIdx' S ∣ r.ramificationIdx' R := by
+  use q.ramificationIdx' R
+  rw [mul_comm, ← ramificationIdx'_tower]
+
+theorem ramificationIdx'_below_le [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T] :
+    q.ramificationIdx' R ≤ r.ramificationIdx' R :=
+  Nat.le_of_dvd (r.ramificationIdx'_pos R) (q.ramificationIdx'_below_dvd r)
+
+theorem ramificationIdx'_above_le [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T] :
+    r.ramificationIdx' S ≤ r.ramificationIdx' R :=
+  Nat.le_of_dvd (r.ramificationIdx'_pos R) (q.ramificationIdx'_above_dvd r)
+
 variable (R) in
 open Pointwise in
 @[simp]