-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
lemma Algebra.intTrace_eq_trace [Module.Free A B] : Algebra.intTrace A B = Algebra.trace A B

Proof state:
case h
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
inst✝ : Module.Free A B
x : B
this✝ : IsIntegralClosure B A (FractionRing B)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ (intTrace A B) x = (trace A B) x

Tactic:
apply IsFractionRing.injective A (FractionRing A)

Result:
case h.a
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
inst✝ : Module.Free 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) = (algebraMap A (FractionRing A)) ((trace A B) x)

Proof state:
case h
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
inst✝ : Module.Free A B
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ (intTrace A B) x = (trace A B) x

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

Result:
case h
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
inst✝ : Module.Free A B
x : B
this✝ : IsIntegralClosure B A (FractionRing B)
this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)
⊢ (intTrace A B) x = (trace A 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
inst✝ : Module.Free A B
⊢ intTrace A B = trace A B

Tactic:
ext x

Result:
case h
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
inst✝ : Module.Free A B
x : B
⊢ (intTrace A B) x = (trace A B) x

Proof state:
case h
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
inst✝ : Module.Free A B
x : B
⊢ (intTrace A B) x = (trace A B) x

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

Result:
case h
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
inst✝ : Module.Free A B
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ (intTrace A B) x = (trace A B) x

Proof state:
case h.a
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
inst✝ : Module.Free 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) = (algebraMap A (FractionRing A)) ((trace A B) x)

Tactic:
rw [Algebra.algebraMap_intTrace_fractionRing, Algebra.trace_localization A A⁰]

Result:
no goals