-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.algebraMap_intTrace_fractionRing (x : B) :
    algebraMap A (FractionRing A) (Algebra.intTrace A B x) =
      Algebra.trace (FractionRing A) (FractionRing B) (algebraMap B _ x)

Proof state:
A : Type u_1
B : Type u_4
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
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 (FractionRing A)) ((intTrace A B) x) =
    (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)

Tactic:
exact Algebra.map_intTraceAux x

Result:
no goals

Proof state:
A : Type u_1
B : Type u_4
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
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 (FractionRing A)) ((intTrace A B) x) =
    (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing B) :=
  Module.Finite_of_isLocalization A B _ _ A⁰

Result:
A : Type u_1
B : Type u_4
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
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 (FractionRing A)) ((intTrace A B) x) =
    (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)

Proof state:
A : Type u_1
B : Type u_4
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
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 (FractionRing A)) ((intTrace A B) x) =
    (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)

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

Result:
A : Type u_1
B : Type u_4
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
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 (FractionRing A)) ((intTrace A B) x) =
    (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)

Proof state:
A : Type u_1
B : Type u_4
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
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 (FractionRing A)) ((intTrace A B) x) =
    (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)

Tactic:
haveI : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
  IsIntegralClosure.isLocalization _ (FractionRing A) _ _

Result:
A : Type u_1
B : Type u_4
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
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 (FractionRing A)) ((intTrace A B) x) =
    (trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)