-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.algebraMap_intTrace (x : B) :
    algebraMap A K (Algebra.intTrace A B x) = Algebra.trace K L (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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A 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) ((intTrace A B) x)) =
    (FractionRing.algEquiv A K).symm ((trace K L) ((algebraMap B L) x))

Tactic:
rw [AlgEquiv.commutes, Algebra.intTrace, Algebra.map_intTraceAux,
  ← 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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A 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
⊢ (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x) =
    (FractionRing.algEquiv A K).symm ((trace K L) ((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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A B
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ (algebraMap A K) ((intTrace A B) x) = (trace K L) ((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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A B
x : B
this✝ : IsIntegralClosure B A (FractionRing B)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ (algebraMap A K) ((intTrace A B) x) = (trace K L) ((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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A B
x : B
⊢ (algebraMap A K) ((intTrace A B) x) = (trace K L) ((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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A B
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ (algebraMap A K) ((intTrace A B) x) = (trace K L) ((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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A 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) ((intTrace A B) x) = (trace K L) ((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✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : NoZeroSMulDivisors A 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) ((intTrace A B) x)) =
    (FractionRing.algEquiv A K).symm ((trace K L) ((algebraMap B L) x))