-- 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)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing B) :=
  Module.Finite_of_isLocalization A B _ _ 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)
this : FiniteDimensional (FractionRing A) (FractionRing B)
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

Proof state:
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))

Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, ← AlgEquiv.coe_ringHom_commutes, RingHom.comp_assoc,
  AlgHom.comp_algebraMap_of_tower, ← IsScalarTower.algebraMap_eq, RingHom.comp_assoc]

Result:
no goals

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
⊢ (algebraMap A K) ((intNorm A B) x) = (norm K) ((algebraMap B L) x)

Tactic:
haveI : IsIntegralClosure B A (FractionRing B) :=
  IsIntegralClosure.of_isIntegrallyClosed _ _ _

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)
⊢ (algebraMap A K) ((intNorm A B) x) = (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)
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)

Tactic:
apply (FractionRing.algEquiv A K).symm.injective

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