-- 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:
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)
⊢ (algebraMap A K) ((intTrace A B) x) = (trace K L) ((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✝⁵ : 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)

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
⊢ (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)))

Tactic:
apply Algebra.trace_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✝⁵ : 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 K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv =
    (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))

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✝⁵ : 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 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:
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✝⁵ : 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 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✝⁵ : 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 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))