Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
f : (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) (under R r)) ≃ₐ[Localization.AtPrime r]
  TensorProduct (Localization.AtPrime q) (Localization.AtPrime r)
    (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r)) :=
  (quotientEquivAlgOfEq (Localization.AtPrime r) ⋯).trans
    (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
      (map (algebraMap R (Localization.AtPrime q)) (under R r)))
⊢ (Module.length (Localization.AtPrime q)
          (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r))).toNat *
      (Module.length (Localization.AtPrime r)
          (Localization.AtPrime r ⧸
            map
              ((algebraMap (Localization.AtPrime q) (Localization.AtPrime r)).comp
                (algebraMap S (Localization.AtPrime q)))
              q)).toNat =
    (Module.length (Localization.AtPrime q)
          (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r))).toNat *
      (Module.length (Localization.AtPrime r)
          (Localization.AtPrime r ⧸ map (algebraMap S (Localization.AtPrime r)) q)).toNat

Tactic:
← IsScalarTower.algebraMap_eq

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
f : (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) (under R r)) ≃ₐ[Localization.AtPrime r]
  TensorProduct (Localization.AtPrime q) (Localization.AtPrime r)
    (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r)) :=
  (quotientEquivAlgOfEq (Localization.AtPrime r) ⋯).trans
    (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
      (map (algebraMap R (Localization.AtPrime q)) (under R r)))
⊢ (Module.length (Localization.AtPrime q)
          (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r))).toNat *
      (Module.length (Localization.AtPrime r)
          (Localization.AtPrime r ⧸ map (algebraMap S (Localization.AtPrime r)) q)).toNat =
    (Module.length (Localization.AtPrime q)
          (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R r))).toNat *
      (Module.length (Localization.AtPrime r)
          (Localization.AtPrime r ⧸ map (algebraMap S (Localization.AtPrime r)) q)).toNat