-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.algebraMap_intNorm (x : B) :
    algebraMap A K (Algebra.intNorm A B x) = Algebra.norm K (algebraMap B L x)

Proof state:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁰ : CommRing A
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A B L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : FiniteDimensional K L
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

Tactic:
haveI : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
  IsIntegralClosure.isLocalization _ (FractionRing A) _ _

Result:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁰ : CommRing A
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A B L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : FiniteDimensional K L
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
x : B
this✝ : IsIntegralClosure B A (FractionRing B)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

Proof state:
case a.he
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁰ : CommRing A
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A B L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : FiniteDimensional K L
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
x : B
this✝² : IsIntegralClosure B A (FractionRing B)
this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : IsFractionRing B L
⊢ (algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv =
    (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))

Tactic:
apply IsLocalization.ringHom_ext A⁰

Result:
case a.he.h
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁰ : CommRing A
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : IsFractionRing A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A B L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsIntegralClosure B A L
inst✝⁷ : FiniteDimensional K L
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDomain B
inst✝³ : IsIntegrallyClosed B
inst✝² : Module.Finite A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
x : B
this✝² : IsIntegralClosure B A (FractionRing B)
this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : IsFractionRing B L
⊢ ((algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv).comp (algebraMap A (FractionRing A)) =
    ((↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))).comp
      (algebraMap A (FractionRing A))