-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.intNorm_eq_of_isLocalization (x : B) :
    algebraMap A Aₘ (Algebra.intNorm A B x) = Algebra.intNorm Aₘ Bₘ (algebraMap B Bₘ x)

Proof state:
A : Type u_1
B : Type u_4
inst✝²⁶ : CommRing A
inst✝²⁵ : CommRing B
inst✝²⁴ : Algebra A B
Aₘ : Type u_5
Bₘ : Type u_6
inst✝²³ : CommRing Aₘ
inst✝²² : CommRing Bₘ
inst✝²¹ : Algebra Aₘ Bₘ
inst✝²⁰ : Algebra A Aₘ
inst✝¹⁹ : Algebra B Bₘ
inst✝¹⁸ : Algebra A Bₘ
inst✝¹⁷ : IsScalarTower A Aₘ Bₘ
inst✝¹⁶ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹⁵ : IsLocalization M Aₘ
inst✝¹⁴ : IsLocalization (algebraMapSubmonoid B M) Bₘ
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)
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : NoZeroSMulDivisors Aₘ Bₘ
inst✝¹ : Module.Finite Aₘ Bₘ
inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_4 := FractionRing B
this✝⁴ : IsIntegralClosure B A L
this✝³ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝² : Algebra Aₘ K := f.toAlgebra
this✝¹ : IsScalarTower A Aₘ K
this✝ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this : Algebra Bₘ L := g.toAlgebra
⊢ algebraMap B L = (algebraMap Bₘ L).comp (algebraMap B Bₘ)

Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]

Result:
no goals

Proof state:
case neg
A : Type u_1
B : Type u_4
inst✝²⁶ : CommRing A
inst✝²⁵ : CommRing B
inst✝²⁴ : Algebra A B
Aₘ : Type u_5
Bₘ : Type u_6
inst✝²³ : CommRing Aₘ
inst✝²² : CommRing Bₘ
inst✝²¹ : Algebra Aₘ Bₘ
inst✝²⁰ : Algebra A Aₘ
inst✝¹⁹ : Algebra B Bₘ
inst✝¹⁸ : Algebra A Bₘ
inst✝¹⁷ : IsScalarTower A Aₘ Bₘ
inst✝¹⁶ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹⁵ : IsLocalization M Aₘ
inst✝¹⁴ : IsLocalization (algebraMapSubmonoid B M) Bₘ
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)
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : NoZeroSMulDivisors Aₘ Bₘ
inst✝¹ : Module.Finite Aₘ Bₘ
inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_4 := FractionRing B
this✝³ : IsIntegralClosure B A L
this✝² : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝¹ : Algebra Aₘ K := f.toAlgebra
this✝ : IsScalarTower A Aₘ K
this : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
letI := g.toAlgebra

Result:
case neg
A : Type u_1
B : Type u_4
inst✝²⁶ : CommRing A
inst✝²⁵ : CommRing B
inst✝²⁴ : Algebra A B
Aₘ : Type u_5
Bₘ : Type u_6
inst✝²³ : CommRing Aₘ
inst✝²² : CommRing Bₘ
inst✝²¹ : Algebra Aₘ Bₘ
inst✝²⁰ : Algebra A Aₘ
inst✝¹⁹ : Algebra B Bₘ
inst✝¹⁸ : Algebra A Bₘ
inst✝¹⁷ : IsScalarTower A Aₘ Bₘ
inst✝¹⁶ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹⁵ : IsLocalization M Aₘ
inst✝¹⁴ : IsLocalization (algebraMapSubmonoid B M) Bₘ
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)
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : NoZeroSMulDivisors Aₘ Bₘ
inst✝¹ : Module.Finite Aₘ Bₘ
inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_4 := FractionRing B
this✝⁴ : IsIntegralClosure B A L
this✝³ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝² : Algebra Aₘ K := f.toAlgebra
this✝¹ : IsScalarTower A Aₘ K
this✝ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this : Algebra Bₘ L := g.toAlgebra
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

Proof state:
case neg
A : Type u_1
B : Type u_4
inst✝²⁶ : CommRing A
inst✝²⁵ : CommRing B
inst✝²⁴ : Algebra A B
Aₘ : Type u_5
Bₘ : Type u_6
inst✝²³ : CommRing Aₘ
inst✝²² : CommRing Bₘ
inst✝²¹ : Algebra Aₘ Bₘ
inst✝²⁰ : Algebra A Aₘ
inst✝¹⁹ : Algebra B Bₘ
inst✝¹⁸ : Algebra A Bₘ
inst✝¹⁷ : IsScalarTower A Aₘ Bₘ
inst✝¹⁶ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹⁵ : IsLocalization M Aₘ
inst✝¹⁴ : IsLocalization (algebraMapSubmonoid B M) Bₘ
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)
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : NoZeroSMulDivisors Aₘ Bₘ
inst✝¹ : Module.Finite Aₘ Bₘ
inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_4 := FractionRing B
this✝² : IsIntegralClosure B A L
this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝ : Algebra Aₘ K := f.toAlgebra
this : IsScalarTower A Aₘ K
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)

Tactic:
letI := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K

Result:
case neg
A : Type u_1
B : Type u_4
inst✝²⁶ : CommRing A
inst✝²⁵ : CommRing B
inst✝²⁴ : Algebra A B
Aₘ : Type u_5
Bₘ : Type u_6
inst✝²³ : CommRing Aₘ
inst✝²² : CommRing Bₘ
inst✝²¹ : Algebra Aₘ Bₘ
inst✝²⁰ : Algebra A Aₘ
inst✝¹⁹ : Algebra B Bₘ
inst✝¹⁸ : Algebra A Bₘ
inst✝¹⁷ : IsScalarTower A Aₘ Bₘ
inst✝¹⁶ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹⁵ : IsLocalization M Aₘ
inst✝¹⁴ : IsLocalization (algebraMapSubmonoid B M) Bₘ
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)
inst✝⁶ : IsDomain Aₘ
inst✝⁵ : IsIntegrallyClosed Aₘ
inst✝⁴ : IsDomain Bₘ
inst✝³ : IsIntegrallyClosed Bₘ
inst✝² : NoZeroSMulDivisors Aₘ Bₘ
inst✝¹ : Module.Finite Aₘ Bₘ
inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_4 := FractionRing B
this✝³ : IsIntegralClosure B A L
this✝² : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝¹ : Algebra Aₘ K := f.toAlgebra
this✝ : IsScalarTower A Aₘ K
this : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
⊢ (algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)