-- 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
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst_9 : CommRing Rₘ
inst_10 : Algebra R Rₘ
inst_11 : CommRing Sₘ
inst_12 : Algebra S Sₘ
inst_13 : Algebra Rₘ Sₘ
inst_14 : Algebra R Sₘ
inst_15 : IsScalarTower R Rₘ Sₘ
inst_16 : IsScalarTower R S Sₘ
inst_17 : IsLocalization M Rₘ
inst_18 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_19 : IsIntegrallyClosed Rₘ
inst_20 : IsDomain Rₘ
inst_21 : IsDomain Sₘ
inst_22 : IsTorsionFree Rₘ Sₘ
inst_23 : Module.Finite Rₘ Sₘ
inst_24 : IsIntegrallyClosed Sₘ
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map (M := Algebra.algebraMapSubmonoid S M) (T := S⁰) L (RingHom.id S) ⋯
algInst : Algebra Rₘ K := f.toAlgebra
algInst_1 : Algebra Sₘ L := g.toAlgebra
algInst_2 : Algebra Rₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
scalarTowerInst : IsScalarTower Rₘ K L := ⋯
this_1 : IsScalarTower R Rₘ K
h : IsFractionRing Rₘ K := ⋯
this_2 : IsScalarTower S Sₘ L
this : IsScalarTower Rₘ Sₘ L
h_1 : IsFractionRing Sₘ L := ⋯
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ (↑M : Set R)
has :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
    (Algebra.norm K : (a : L) → K) ((algebraMap S L : (a : S) → L) a)
refine_1 :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((algebraMap R Rₘ : (a : R) → Rₘ) s) : K)
        (finrank K L)) =
    ((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R))
refine_1₁ :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
    ((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R))
refine_1₂ :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
    (algebraMap R K : (a : R) → K) ((Algebra.intNorm R S : (a : S) → R) a)
refine_1₃ refine_1₄ refine_1₅ refine_1₆ :
  HMul.hMul (α := K) ((Algebra.norm K : (a : L) → K) (((algebraMap Sₘ L : Sₘ →+* L) : (a : Sₘ) → L) a') : K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) s : K) (finrank K L)) =
    (Algebra.norm K : (a : L) → K) ((algebraMap S L : (a : S) → L) a)
⊢ HMul.hMul (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((Algebra.intNorm Rₘ Sₘ : (a : Sₘ) → Rₘ) a') : K)
      (HPow.hPow (α := K) (((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K) ((algebraMap R Rₘ : (a : R) → Rₘ) s) : K)
        (finrank K L)) =
    ((algebraMap Rₘ K : Rₘ →+* K) : (a : Rₘ) → K)
      ((algebraMap R Rₘ : (a : R) → Rₘ) ((Algebra.intNorm R S : (a : S) → R) a : R))

Tactic:
rwa [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intNorm (L := L)]

Premises used: Algebra.algebraMap_intNorm, IsScalarTower.algebraMap_apply