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
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)
    ((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)
have 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)))
Tactic: apply Algebra.trace_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
    (FractionRing.algEquiv B L).toRingEquiv
-- 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 (α := 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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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
⊢ 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)
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
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)
⊢ 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)
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
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)
⊢ 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)
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
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)
⊢ 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)
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 (goal)
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
⊢ Eq (α := B →ₗ[A] A) (intTrace A B) (trace A B)
have h : ∀ (x : B), Eq.{u_1 + 1} (α := A) ((intTrace A B : (a : B) → A) x : A) ((trace A B : (a : B) → A) x : A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := A) ((intTrace A B : (a : B) → A) x : A) ((trace A B : (a : B) → A) x : A)
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
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)
⊢ Eq.{u_1 + 1} (α := A) ((intTrace A B : (a : B) → A) x : A) ((trace A B : (a : B) → A) x : A)
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
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)
⊢ Eq.{u_1 + 1} (α := A) ((intTrace A B : (a : B) → A) x : A) ((trace A B : (a : B) → A) x : A)
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 (goal)
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)
⊢ Eq.{u_1 + 1} (α := A) ((intTrace A B : (a : B) → A) x : A) ((trace A B : (a : B) → A) x : A)
have 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)
Tactic: apply IsFractionRing.injective A (FractionRing A)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Algebra.algebraMap_intTrace_fractionRing, Algebra.trace_localization A A⁰]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Algebra.algebraMap_intTrace_fractionRing, Algebra.trace_localization A A⁰]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Module.Finite Aₘ Bₘ
x : B
⊢ Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
    ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
have pos : ∀ (hM : 0 ∈ M),
  Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
    ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
Tactic: by_cases hM : 0 ∈ M
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Module.Finite Aₘ Bₘ
x : B
pos :
  ∀ (hM : 0 ∈ M),
    Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
      ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
⊢ Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
    ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
have neg : ∀ (hM : 0 ∉ M),
  Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
    ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
Tactic: by_cases hM : 0 ∈ M
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Module.Finite Aₘ Bₘ
x : B
hM : 0 ∉ M
⊢ Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
    ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
have hM₁ : M ≤ A⁰
Tactic: replace hM : M ≤ A⁰ := fun x hx ↦ mem_nonZeroDivisors_iff_ne_zero.mpr (fun e ↦ hM (e ▸ hx))
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
⊢ Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
    ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
have this : IsIntegralClosure B A L
Tactic: have : IsIntegralClosure B A L :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (hypothesis)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this : IsIntegralClosure B A L
⊢ Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
    ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
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
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this_1 : IsIntegralClosure B A L
this : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
    ((intTrace Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)
have this₁ : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
Tactic: have : IsLocalization (algebraMapSubmonoid B A⁰) L :=
    IsIntegralClosure.isLocalization _ (FractionRing A) _ _
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this_1 : IsIntegralClosure B A L
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this : Algebra Aₘ K := f.toAlgebra
⊢ Eq (α := A →+* K) (algebraMap A K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ K) (algebraMap A Aₘ))
have rw : Eq (α := A →+* K) (algebraMap A K) (f.comp (algebraMap A Aₘ))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]