awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : CommRing B₃
inst_4 : Algebra A B
inst_5 : Algebra A B₂
inst_6 : Algebra A B₃
inst_7 : Field K
inst_8 : Field L
inst_9 : Field L₂
inst_10 : Field L₃
inst_11 : Algebra A K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A K L
inst_15 : Algebra K L₂
inst_16 : Algebra A L₂
inst_17 : IsScalarTower A K L₂
inst_18 : Algebra K L₃
inst_19 : Algebra A L₃
inst_20 : IsScalarTower A K L₃
inst_21 : Algebra B L
inst_22 : IsScalarTower A B L
inst_23 : IsIntegralClosure B A L
inst_24 : Algebra B₂ L₂
inst_25 : IsScalarTower A B₂ L₂
inst_26 : IsIntegralClosure B₂ A L₂
inst_27 : Algebra B₃ L₃
inst_28 : IsScalarTower A B₃ L₃
inst_29 : IsIntegralClosure B₃ A L₃
σ : L →ₐ[K] L₂
σ' : L₂ →ₐ[K] L₃
⊢ Eq (α := B →ₐ[A] B₃) (galRestrict' A B B₃ (σ'.comp σ)) (AlgHom.comp (galRestrict' A B₂ B₃ σ') (galRestrict' A B B₂ σ))
have H : ∀ (x : B),
  Eq.{u_8 + 1} (α := B₃) ((galRestrict' A B B₃ (σ'.comp σ) : (a : B) → B₃) x : B₃)
    ((AlgHom.comp (galRestrict' A B₂ B₃ σ') (galRestrict' A B B₂ σ) : (a : B) → B₃) x : B₃)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : CommRing B₃
inst_4 : Algebra A B
inst_5 : Algebra A B₂
inst_6 : Algebra A B₃
inst_7 : Field K
inst_8 : Field L
inst_9 : Field L₂
inst_10 : Field L₃
inst_11 : Algebra A K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A K L
inst_15 : Algebra K L₂
inst_16 : Algebra A L₂
inst_17 : IsScalarTower A K L₂
inst_18 : Algebra K L₃
inst_19 : Algebra A L₃
inst_20 : IsScalarTower A K L₃
inst_21 : Algebra B L
inst_22 : IsScalarTower A B L
inst_23 : IsIntegralClosure B A L
inst_24 : Algebra B₂ L₂
inst_25 : IsScalarTower A B₂ L₂
inst_26 : IsIntegralClosure B₂ A L₂
inst_27 : Algebra B₃ L₃
inst_28 : IsScalarTower A B₃ L₃
inst_29 : IsIntegralClosure B₃ A L₃
σ : L →ₐ[K] L₂
σ' : L₂ →ₐ[K] L₃
x : B
⊢ Eq.{u_8 + 1} (α := B₃) ((galRestrict' A B B₃ (σ'.comp σ) : (a : B) → B₃) x : B₃)
    ((AlgHom.comp (galRestrict' A B₂ B₃ σ') (galRestrict' A B B₂ σ) : (a : B) → B₃) x : B₃)
have H : Eq.{u_5 + 1} (α := ↥(integralClosure A L₃))
  (((AlgEquiv.symm (IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃) :
          AlgEquiv.{u_1, u_8, u_5} A B₃ ↥(integralClosure A L₃)) :
        (a : B₃) → ↥(integralClosure A L₃))
      ((galRestrict' A B B₃ (σ'.comp σ) : (a : B) → B₃) x) :
    ↥(integralClosure A L₃))
  (((AlgEquiv.symm (IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃) :
          AlgEquiv.{u_1, u_8, u_5} A B₃ ↥(integralClosure A L₃)) :
        (a : B₃) → ↥(integralClosure A L₃))
      ((AlgHom.comp (galRestrict' A B₂ B₃ σ') (galRestrict' A B B₂ σ) : (a : B) → B₃) x) :
    ↥(integralClosure A L₃))
Tactic: apply (IsIntegralClosure.equiv A (integralClosure A L₃) L₃ B₃).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : CommRing B₃
inst_4 : Algebra A B
inst_5 : Algebra A B₂
inst_6 : Algebra A B₃
inst_7 : Field K
inst_8 : Field L
inst_9 : Field L₂
inst_10 : Field L₃
inst_11 : Algebra A K
inst_12 : Algebra K L
inst_13 : Algebra A L
inst_14 : IsScalarTower A K L
inst_15 : Algebra K L₂
inst_16 : Algebra A L₂
inst_17 : IsScalarTower A K L₂
inst_18 : Algebra K L₃
inst_19 : Algebra A L₃
inst_20 : IsScalarTower A K L₃
inst_21 : Algebra B L
inst_22 : IsScalarTower A B L
inst_23 : IsIntegralClosure B A L
inst_24 : Algebra B₂ L₂
inst_25 : IsScalarTower A B₂ L₂
inst_26 : IsIntegralClosure B₂ A L₂
inst_27 : Algebra B₃ L₃
inst_28 : IsScalarTower A B₃ L₃
inst_29 : IsIntegralClosure B₃ A L₃
σ : L →ₐ[K] L₂
σ' : L₂ →ₐ[K] L₃
x : B
⊢ Eq.{u_5 + 1} (α := ↥(integralClosure A L₃))
    (((AlgEquiv.symm (IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃) :
            AlgEquiv.{u_1, u_8, u_5} A B₃ ↥(integralClosure A L₃)) :
          (a : B₃) → ↥(integralClosure A L₃))
        ((galRestrict' A B B₃ (σ'.comp σ) : (a : B) → B₃) x) :
      ↥(integralClosure A L₃))
    (((AlgEquiv.symm (IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃) :
            AlgEquiv.{u_1, u_8, u_5} A B₃ ↥(integralClosure A L₃)) :
          (a : B₃) → ↥(integralClosure A L₃))
        ((AlgHom.comp (galRestrict' A B₂ B₃ σ') (galRestrict' A B B₂ σ) : (a : B) → B₃) x) :
      ↥(integralClosure A L₃))
have H : Eq.{u_5 + 1} (α := L₃)
  (↑(((AlgEquiv.symm (IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃) :
            AlgEquiv.{u_1, u_8, u_5} A B₃ ↥(integralClosure A L₃)) :
          (a : B₃) → ↥(integralClosure A L₃))
        ((galRestrict' A B B₃ (σ'.comp σ) : (a : B) → B₃) x)) :
    L₃)
  (↑(((AlgEquiv.symm (IsIntegralClosure.equiv A (↥(integralClosure A L₃)) L₃ B₃) :
            AlgEquiv.{u_1, u_8, u_5} A B₃ ↥(integralClosure A L₃)) :
          (a : B₃) → ↥(integralClosure A L₃))
        ((AlgHom.comp (galRestrict' A B₂ B₃ σ') (galRestrict' A B B₂ σ) : (a : B) → B₃) x)) :
    L₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : CommRing B₃
inst_4 : Algebra A B
inst_5 : Algebra A B₂
inst_6 : Algebra A B₃
inst_7 : Field K
inst_8 : Field L
inst_9 : Field L₂
inst_10 : Field L₃
inst_11 : Algebra A K
inst_12 : IsFractionRing A K
inst_13 : Algebra K L
inst_14 : Algebra A L
inst_15 : IsScalarTower A K L
inst_16 : Algebra K L₂
inst_17 : Algebra A L₂
inst_18 : IsScalarTower A K L₂
inst_19 : Algebra K L₃
inst_20 : Algebra A L₃
inst_21 : IsScalarTower A K L₃
inst_22 : Algebra B L
inst_23 : IsScalarTower A B L
inst_24 : IsIntegralClosure B A L
inst_25 : Algebra B₂ L₂
inst_26 : IsScalarTower A B₂ L₂
inst_27 : IsIntegralClosure B₂ A L₂
inst_28 : Algebra B₃ L₃
inst_29 : IsScalarTower A B₃ L₃
inst_30 : IsIntegralClosure B₃ A L₃
inst_31 : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this_1 : IsDomain A
this_2 : IsTorsionFree A L₂
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
H :
  ∀ (y : ↥(Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰)),
    IsUnit.{u_4} (M := L₂)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B₂ L₂) (↑σ : B →+* B₂) : (a : B) → L₂)
          (↑y : B) :
        L₂)
⊢ Eq (α := K →+* L₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.lift H) (algebraMap K L))
    (algebraMap K L₂)
have h : Eq (α := A →+* L₂)
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.lift H) (algebraMap K L)) (algebraMap A K))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L₂) (algebraMap A K))
Tactic: apply IsLocalization.ringHom_ext A⁰
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : CommRing B₃
inst_4 : Algebra A B
inst_5 : Algebra A B₂
inst_6 : Algebra A B₃
inst_7 : Field K
inst_8 : Field L
inst_9 : Field L₂
inst_10 : Field L₃
inst_11 : Algebra A K
inst_12 : IsFractionRing A K
inst_13 : Algebra K L
inst_14 : Algebra A L
inst_15 : IsScalarTower A K L
inst_16 : Algebra K L₂
inst_17 : Algebra A L₂
inst_18 : IsScalarTower A K L₂
inst_19 : Algebra K L₃
inst_20 : Algebra A L₃
inst_21 : IsScalarTower A K L₃
inst_22 : Algebra B L
inst_23 : IsScalarTower A B L
inst_24 : IsIntegralClosure B A L
inst_25 : Algebra B₂ L₂
inst_26 : IsScalarTower A B₂ L₂
inst_27 : IsIntegralClosure B₂ A L₂
inst_28 : Algebra B₃ L₃
inst_29 : IsScalarTower A B₃ L₃
inst_30 : IsIntegralClosure B₃ A L₃
inst_31 : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this_1 : IsDomain A
this_2 : IsTorsionFree A L₂
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
H :
  ∀ (y : ↥(Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰)),
    IsUnit.{u_4} (M := L₂)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B₂ L₂) (↑σ : B →+* B₂) : (a : B) → L₂)
          (↑y : B) :
        L₂)
⊢ Eq (α := A →+* L₂)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.lift H) (algebraMap K L)) (algebraMap A K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L₂) (algebraMap A K))
have h : ∀ (x : A),
  Eq.{u_4 + 1} (α := L₂)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.lift H) (algebraMap K L))
            (algebraMap A K) :
          (a : A) → L₂)
        x :
      L₂)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L₂) (algebraMap A K) : (a : A) → L₂) x : L₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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 : Algebra.IsAlgebraic K L
⊢ Eq (α := L →ₐ[K] L) (galLift K L L (AlgHom.id A B)) (AlgHom.id K L)
have H : ∀ (x : L), Eq (α := L) ((galLift K L L (AlgHom.id A B) : (a : L) → L) x : L) ((AlgHom.id K L : (a : L) → L) x : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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 : IsGalois K L
inst_15 : IsIntegrallyClosed A
x : B
⊢ Eq.{u_6 + 1} (α := B)
    (∏ σ : Gal(L/K),
        ((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
              B ≃ₐ[A] B) :
            (a : B) → B)
          x :
      B)
    ((algebraMap A B : (a : A) → B)
        (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
          ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
      B)
have a : Eq.{u_3 + 1} (α := L)
  ((algebraMap B L : (a : B) → L)
      (∏ σ : Gal(L/K),
        ((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
              B ≃ₐ[A] B) :
            (a : B) → B)
          x) :
    L)
  ((algebraMap B L : (a : B) → L)
      ((algebraMap A B : (a : A) → B)
          (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
            ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) sorry) :
        B) :
    L)
Tactic: apply IsIntegralClosure.algebraMap_injective B A L
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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 : IsGalois K L
inst_15 : IsIntegrallyClosed A
x : B
⊢ Eq.{u_3 + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        (∏ σ : Gal(L/K),
          ((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
                B ≃ₐ[A] B) :
              (a : B) → B)
            x) :
      L)
    ((algebraMap B L : (a : B) → L)
        ((algebraMap A B : (a : A) → B)
            (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
              ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
          B) :
      L)
have a : Eq.{u_3 + 1} (α := L)
  ((algebraMap B L : (a : B) → L)
      (∏ σ : Gal(L/K),
        ((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
              B ≃ₐ[A] B) :
            (a : B) → B)
          x) :
    L)
  ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap A K) : (a : A) → L)
      (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
        ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) sorry) :
    L)
Tactic: rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_eq A K L]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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
⊢ 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)
have this : IsIntegralClosure B A (FractionRing B)
Tactic: haveI : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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)
⊢ 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)
have this₁ : 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) ..
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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)
⊢ 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)
have this₁ : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) (FractionRing B)
Tactic: haveI : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
    IsIntegralClosure.isLocalization _ (FractionRing A) _ _
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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)
⊢ 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)
have this₁ : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
Tactic: haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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)
⊢ 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)
have this₁ : IsFractionRing B L
Tactic: haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
⊢ 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)
have 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: apply (FractionRing.algEquiv A K).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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
⊢ 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)
have 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)
Tactic: rw [AlgEquiv.commutes, Algebra.intTrace, Algebra.map_intTraceAux,
    ← AlgEquiv.commutes (FractionRing.algEquiv B L)]