awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)

Tactic:
haveI : Algebra.IsAlgebraic (FractionRing A) (FractionRing B) :=
    isAlgebraic_of_isFractionRing (R := A) (S := B) ..
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)

Tactic:
haveI : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
    IsIntegralClosure.isLocalization _ (FractionRing A) _ _
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
⊢ FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ IsFractionRing B L

Tactic:
haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsFractionRing B L
a :
  Eq.{u_1 + 1} (α := FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((algebraMap A K : (a : A) → K) ((intTrace A B : (a : B) → A) x : A)) :
      FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((trace K L : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L)) :
      FractionRing A)
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((intTrace A B : (a : B) → A) x : A) : K)
    ((trace K L : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K)

Tactic:
apply (FractionRing.algEquiv A K).symm.injective

Premises used: AlgEquiv.symm, FractionRing.algEquiv, AlgEquiv.injective
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsFractionRing B L
a :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((trace K L : (a : L) → K)
          ((FractionRing.algEquiv B L : (a : FractionRing B) → L)
              ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x : FractionRing B) :
            L)) :
      FractionRing A)
⊢ Eq.{u_1 + 1} (α := FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((algebraMap A K : (a : A) → K) ((intTrace A B : (a : B) → A) x : A)) :
      FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((trace K L : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L)) :
      FractionRing A)

Tactic:
rw [AlgEquiv.commutes, Algebra.intTrace, Algebra.map_intTraceAux,
    ← AlgEquiv.commutes (FractionRing.algEquiv B L)]

Premises used: AlgEquiv.commutes, Algebra.intTrace, FractionRing.algEquiv, Algebra.map_intTraceAux
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsFractionRing B L
a :
  Eq (α := RingHom.{u_1, u_3} (FractionRing A) L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
      (algebraMap (FractionRing A) (FractionRing B)))
⊢ Eq.{u_1 + 1} (α := FractionRing A)
    ((trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((trace K L : (a : L) → K)
          ((FractionRing.algEquiv B L : (a : FractionRing B) → L)
              ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x : FractionRing B) :
            L)) :
      FractionRing A)

Tactic:
apply Algebra.trace_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
    (FractionRing.algEquiv B L).toRingEquiv

Premises used: FractionRing.algEquiv, AlgEquiv.toRingEquiv, Algebra.trace_eq_of_equiv_equiv
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsFractionRing B L
a :
  ∀ (x : FractionRing A),
    Eq.{u_3 + 1} (α := L)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
              (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
            (a : FractionRing A) → L)
          x :
        L)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
              (algebraMap (FractionRing A) (FractionRing B)) :
            (a : FractionRing A) → L)
          x :
        L)
⊢ Eq (α := RingHom.{u_1, u_3} (FractionRing A) L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
      (algebraMap (FractionRing A) (FractionRing B)))

Tactic:
ext
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsFractionRing B L
x_1 : FractionRing A
⊢ Eq.{u_3 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
          (a : FractionRing A) → L)
        x_1 :
      L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
            (algebraMap (FractionRing A) (FractionRing B)) :
          (a : FractionRing A) → L)
        x_1 :
      L)

Tactic:
IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K) (FractionRing.algEquiv B L) _

Premises used: FractionRing.algEquiv, IsFractionRing.algEquiv_commutes
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsFractionRing B L
x_1 : FractionRing A
⊢ Eq.{u_3 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
          (a : FractionRing A) → L)
        x_1 :
      L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
            (algebraMap (FractionRing A) (FractionRing B)) :
          (a : FractionRing A) → L)
        x_1 :
      L)

Tactic:
exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K) (FractionRing.algEquiv B L) _

Premises used: FractionRing.algEquiv, IsFractionRing.algEquiv_commutes
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
⊢ IsIntegralClosure B A (FractionRing B)

Tactic:
haveI : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)

Tactic:
haveI : Algebra.IsAlgebraic (FractionRing A) (FractionRing B) :=
    isAlgebraic_of_isFractionRing (R := A) (S := B) ..
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)

Tactic:
haveI : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
    IsIntegralClosure.isLocalization _ (FractionRing A) _ _
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
⊢ FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intTrace A B : (a : B) → A) x) : FractionRing A)
    ((trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)

Tactic:
Algebra.map_intTraceAux x

Premises used: Set.Mem, setOf, Algebra.map_intTraceAux
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intTrace A B : (a : B) → A) x) : FractionRing A)
    ((trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)

Tactic:
exact Algebra.map_intTraceAux x

Premises used: Algebra.map_intTraceAux
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : Free A B
h : ∀ (x : B), Eq.{u_1 + 1} (α := A) ((intTrace A B : (a : B) → A) x : A) ((trace A B : (a : B) → A) x : A)
⊢ Eq (α := B →ₗ[A] A) (intTrace A B) (trace A B)

Tactic:
ext x
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : Free A B
x : B
⊢ IsIntegralClosure B A (FractionRing B)

Tactic:
haveI : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : Free A B
x : B
this : IsIntegralClosure B A (FractionRing B)
⊢ Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)

Tactic:
haveI : Algebra.IsAlgebraic (FractionRing A) (FractionRing B) :=
    isAlgebraic_of_isFractionRing (R := A) (S := B) ..
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : Free A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)

Tactic:
haveI : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
    IsIntegralClosure.isLocalization _ (FractionRing A) _ _
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : Free A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
h :
  Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intTrace A B : (a : B) → A) x) : FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((trace A B : (a : B) → A) x) : FractionRing A)
⊢ Eq.{u_1 + 1} (α := A) ((intTrace A B : (a : B) → A) x : A) ((trace A B : (a : B) → A) x : A)

Tactic:
apply IsFractionRing.injective A (FractionRing A)

Premises used: IsFractionRing.injective, FractionRing
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : Free A B
x : B
this_1 : IsIntegralClosure B A (FractionRing B)
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
h :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((trace (FractionRing A) (FractionRing B) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((trace A B : (a : B) → A) x) : FractionRing A)
h₁ h₂ :
  Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((trace A B : (a : B) → A) x) : FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((trace A B : (a : B) → A) x) : FractionRing A)
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intTrace A B : (a : B) → A) x) : FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((trace A B : (a : B) → A) x) : FractionRing A)

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

Premises used: nonZeroDivisors, Algebra.trace_localization, Algebra.algebraMap_intTrace_fractionRing