-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R⁰)
    {Rₘ : Type*} (Sₘ : Type*) [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ]
    [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ]
    [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
    [IsIntegrallyClosed Rₘ] [IsDomain Rₘ] [IsDomain Sₘ] [NoZeroSMulDivisors Rₘ Sₘ]
    [Module.Finite Rₘ Sₘ] [IsIntegrallyClosed Sₘ]
    [Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)] :
    spanNorm Rₘ (I.map (algebraMap S Sₘ)) = (spanNorm R I).map (algebraMap R Rₘ)

Proof state:
case refine_1.intro.mk.intro.mk.intro.intro
R : Type u_1
inst✝²⁶ : CommRing R
inst✝²⁵ : IsDomain R
S : Type u_3
inst✝²⁴ : CommRing S
inst✝²³ : IsDomain S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsIntegrallyClosed S
inst✝²⁰ : Algebra R S
inst✝¹⁹ : Module.Finite R S
inst✝¹⁸ : NoZeroSMulDivisors R S
inst✝¹⁷ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this✝² : IsScalarTower R Rₘ K
x✝¹ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
this✝¹ : IsScalarTower S Sₘ L
this✝ : IsScalarTower Rₘ Sₘ L
x✝ : IsFractionRing Sₘ L :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (Algebra.algebraMapSubmonoid S M) Sₘ L
this : IsIntegralClosure Sₘ Rₘ L
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ ↑M
has : a' * (algebraMap S Sₘ) ↑⟨(algebraMap R S) s, ⋯⟩ = (algebraMap S Sₘ) ↑⟨a, ha⟩
⊢ ∃ a b, (Algebra.intNorm Rₘ Sₘ) a' * (algebraMap R Rₘ) ↑b = (algebraMap R Rₘ) ↑a

Tactic:
refine ⟨⟨Algebra.intNorm R S a, intNorm_mem_spanNorm _ ha⟩,
  ⟨s ^ Module.finrank K L, pow_mem hs _⟩, ?_⟩

Result:
case refine_1.intro.mk.intro.mk.intro.intro
R : Type u_1
inst✝²⁶ : CommRing R
inst✝²⁵ : IsDomain R
S : Type u_3
inst✝²⁴ : CommRing S
inst✝²³ : IsDomain S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsIntegrallyClosed S
inst✝²⁰ : Algebra R S
inst✝¹⁹ : Module.Finite R S
inst✝¹⁸ : NoZeroSMulDivisors R S
inst✝¹⁷ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this✝² : IsScalarTower R Rₘ K
x✝¹ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
this✝¹ : IsScalarTower S Sₘ L
this✝ : IsScalarTower Rₘ Sₘ L
x✝ : IsFractionRing Sₘ L :=
  IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (Algebra.algebraMapSubmonoid S M) Sₘ L
this : IsIntegralClosure Sₘ Rₘ L
a' : Sₘ
a : S
ha : a ∈ I
s : R
hs : s ∈ ↑M
has : a' * (algebraMap S Sₘ) ↑⟨(algebraMap R S) s, ⋯⟩ = (algebraMap S Sₘ) ↑⟨a, ha⟩
⊢ (Algebra.intNorm Rₘ Sₘ) a' * (algebraMap R Rₘ) ↑⟨s ^ Module.finrank K L, ⋯⟩ =
    (algebraMap R Rₘ) ↑⟨(Algebra.intNorm R S) a, ⋯⟩

Proof state:
R : Type u_1
inst✝²⁶ : CommRing R
inst✝²⁵ : IsDomain R
S : Type u_3
inst✝²⁴ : CommRing S
inst✝²³ : IsDomain S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsIntegrallyClosed S
inst✝²⁰ : Algebra R S
inst✝¹⁹ : Module.Finite R S
inst✝¹⁸ : NoZeroSMulDivisors R S
inst✝¹⁷ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)

Tactic:
have : IsScalarTower S Sₘ L := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])

Result:
R : Type u_1
inst✝²⁶ : CommRing R
inst✝²⁵ : IsDomain R
S : Type u_3
inst✝²⁴ : CommRing S
inst✝²³ : IsDomain S
inst✝²² : IsIntegrallyClosed R
inst✝²¹ : IsIntegrallyClosed S
inst✝²⁰ : Algebra R S
inst✝¹⁹ : Module.Finite R S
inst✝¹⁸ : NoZeroSMulDivisors R S
inst✝¹⁷ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
M : Submonoid R
hM : M ≤ R⁰
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹⁶ : CommRing Rₘ
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : CommRing Sₘ
inst✝¹³ : Algebra S Sₘ
inst✝¹² : Algebra Rₘ Sₘ
inst✝¹¹ : Algebra R Sₘ
inst✝¹⁰ : IsScalarTower R Rₘ Sₘ
inst✝⁹ : IsScalarTower R S Sₘ
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝⁶ : IsIntegrallyClosed Rₘ
inst✝⁵ : IsDomain Rₘ
inst✝⁴ : IsDomain Sₘ
inst✝³ : NoZeroSMulDivisors Rₘ Sₘ
inst✝² : Module.Finite Rₘ Sₘ
inst✝¹ : IsIntegrallyClosed Sₘ
inst✝ : Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)
K : Type u_1 := FractionRing R
f : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
L : Type u_3 := FractionRing S
g : Sₘ →+* L := IsLocalization.map L (RingHom.id S) ⋯
algInst✝² : Algebra Rₘ K := f.toAlgebra
algInst✝¹ : Algebra Sₘ L := g.toAlgebra
algInst✝ : Algebra Rₘ L := ((algebraMap K L).comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower Rₘ K L := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap Rₘ L))
this✝ : IsScalarTower R Rₘ K
x✝ : IsFractionRing Rₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
this : IsScalarTower S Sₘ L
⊢ spanNorm Rₘ (map (algebraMap S Sₘ) I) = map (algebraMap R Rₘ) (spanNorm R I)