-- Module: Mathlib.RingTheory.Ideal.Norm.RelNorm
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
K : Type u_1 := FractionRing R
e_s :
  Eq (α := K)
    ((Algebra.norm K : (a : FractionRing S) → K)
        ((algebraMap (Localization (M := S) P') (FractionRing S) : (a : Localization P') → FractionRing S)
          ((algebraMap Rₚ (Localization (M := S) P') : (a : Rₚ) → Localization P')
            (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
e_s₁ :
  Eq (α := K)
    ((Algebra.norm K : (a : FractionRing S) → K)
        ((algebraMap Rₚ (FractionRing S) : (a : Rₚ) → FractionRing S)
          (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
e_s₂ :
  Eq (α := K)
    ((Algebra.norm K : (a : FractionRing S) → K)
        ((algebraMap K (FractionRing S) : (a : K) → FractionRing S)
          ((algebraMap Rₚ K : (a : Rₚ) → K) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)
e_s₃ :
  HPow.hPow (α := K)
      ((algebraMap Rₚ K : (a : Rₚ) → K) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))
      (finrank.{u_1, u_3} K (FractionRing S)) =
    (algebraMap Rₚ K : (a : Rₚ) → K)
      (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
        (finrank.{u_1, u_3} (FractionRing R) (FractionRing S)))
e_s₄ e_s₅ :
  HPow.hPow (α := K)
      ((algebraMap Rₚ K : (a : Rₚ) → K) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))
      (finrank.{u_1, u_3} K (FractionRing S)) =
    HPow.hPow (α := K)
      ((algebraMap Rₚ K : (a : Rₚ) → K) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))
      (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
⊢ Eq (α := K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        ((Algebra.intNorm (Localization.AtPrime P) (Localization (M := S) P') :
            (a : Localization P') → Localization.AtPrime P)
          ((algebraMap Rₚ (Localization (M := S) P') : (a : Rₚ) → Localization P')
            (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I)))) :
      K)
    ((algebraMap Rₚ K : (a : Rₚ) → K)
        (HPow.hPow (α := Rₚ) (IsPrincipal.generator (map (F := R →+* Rₚ) (algebraMap R Rₚ) I))
          (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))) :
      K)

Tactic:
rw [Algebra.algebraMap_intNorm (L := FractionRing S), ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply Rₚ K, Algebra.norm_algebraMap, map_pow]

Premises used: Algebra.algebraMap_intNorm, map_pow, Algebra.norm_algebraMap, IsScalarTower.algebraMap_apply