-- Lean 4 proof step from Mathlib.RingTheory.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 R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst_7 : q.IsPrime
inst_8 : r.IsPrime
inst_9 : r.LiesOver q
inst_10 : Algebra.{u_2, u_3} (Localization.AtPrime q) (Localization.AtPrime r)
inst_11 : Localization.AtPrime.IsLiesOverAlgebra q r
inst_12 : Module.Flat.{u_2, u_3} (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
f : HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
    (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r))
      (under R r)) ≃ₐ[Localization.AtPrime r]
  TensorProduct.{u_2, u_3, u_2} (Localization.AtPrime q) (Localization.AtPrime r)
    (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
      (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) (under R r))) :=
  AlgEquiv.trans (quotientEquivAlgOfEq (Localization.AtPrime r) ⋯)
    (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
      (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q)) (under R r)))
rw :
  (Module.length.{u_3, u_3} (Localization.AtPrime r)
        (HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
          (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r))
            (under R r)))).toNat =
    q.ramificationIdx' R * r.ramificationIdx' S
rw₁ :
  (Module.length.{u_3, u_3} (Localization.AtPrime r)
        (HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
          (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r))
            (under R r)))).toNat =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
          (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
            (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
              (under R r)))).toNat *
      r.ramificationIdx' S
rw₂ :
  (Module.length.{u_3, u_3} (Localization.AtPrime r)
        (HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
          (map (F := RingHom.{u_1, u_3} R (Localization.AtPrime r)) (algebraMap R (Localization.AtPrime r))
            (under R r)))).toNat =
    (Module.length.{u_2, u_2} (Localization.AtPrime q)
          (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
            (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
              (under R r)))).toNat *
      (Module.length.{u_3, u_3} (Localization.AtPrime r)
          (HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
            (map (F := RingHom.{u_2, u_3} S (Localization.AtPrime r)) (algebraMap S (Localization.AtPrime r)) q))).toNat
⊢ r.ramificationIdx' R = q.ramificationIdx' R * r.ramificationIdx' S
have rw₃ : (Module.length (Localization.AtPrime r)
      (TensorProduct.{u_2, u_3, u_2} (Localization.AtPrime q) (Localization.AtPrime r)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
            (under R r))))).toNat =
  (Module.length.{u_2, u_2} (Localization.AtPrime q)
        (HasQuotient.Quotient (Localization.AtPrime q) (B := Ideal (Localization.AtPrime q))
          (map (F := RingHom.{u_1, u_2} R (Localization.AtPrime q)) (algebraMap R (Localization.AtPrime q))
            (under R r)))).toNat *
    (Module.length.{u_3, u_3} (Localization.AtPrime r)
        (HasQuotient.Quotient (Localization.AtPrime r) (B := Ideal (Localization.AtPrime r))
          (map (F := RingHom.{u_2, u_3} S (Localization.AtPrime r)) (algebraMap S (Localization.AtPrime r)) q))).toNat
Tactic: rw [ramificationIdx'_def, ramificationIdx'_eq (r.under R), ramificationIdx'_eq q,
    f.toLinearEquiv.length_eq, IsLocalRing.length_baseChange, ENat.toNat_mul,
    ← Localization.AtPrime.map_eq_maximalIdeal, map_map, ← IsScalarTower.algebraMap_eq]