-- 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:
case a
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
⊢ (FractionRing.algEquiv A K).symm ((algebraMap A K) ((intNorm A B) x)) =
    (FractionRing.algEquiv A K).symm ((norm K) ((algebraMap B L) x))

Tactic:
rw [AlgEquiv.commutes, Algebra.intNorm, Algebra.map_intNormAux,
  ← AlgEquiv.commutes (FractionRing.algEquiv B L)]

Result:
case a
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
⊢ (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x) =
    (FractionRing.algEquiv A K).symm ((norm K) ((FractionRing.algEquiv B L) ((algebraMap B (FractionRing B)) 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)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

Tactic:
haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B

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)
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : IsFractionRing B L
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

Proof state:
case a
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
⊢ (norm (FractionRing A)) ((algebraMap B (FractionRing B)) x) =
    (FractionRing.algEquiv A K).symm ((norm K) ((FractionRing.algEquiv B L) ((algebraMap B (FractionRing B)) x)))

Tactic:
apply Algebra.norm_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
  (FractionRing.algEquiv B L).toRingEquiv

Result:
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))