awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
⊢ IsLocalRing A

Tactic:
have : IsLocalRing A := AtPrime.isLocalRing A q
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
rw :
  Eq.{u_2 + 1} (α := Ideal A) (sInf (Ideal.under R ⁻¹' I.minimalPrimes)) (Ideal.map (F := R →+* A) (algebraMap R A) q)
⊢ Eq.{u_2 + 1} (α := Ideal A) (Ideal.radical (Ideal.map (F := R →+* A) (algebraMap R A) I))
    (Ideal.map (F := R →+* A) (algebraMap R A) q)

Tactic:
rw [← Ideal.sInf_minimalPrimes, IsLocalization.minimalPrimes_map q.primeCompl A I]

Premises used: IsLocalization.minimalPrimes_map, Ideal.primeCompl, Ideal.sInf_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Eq.{u_2 + 1} (α := Ideal A) (sInf (Ideal.under R ⁻¹' I.minimalPrimes)) (Ideal.map (F := R →+* A) (algebraMap R A) q)

Tactic:
le_antisymm (sInf_le ?_) (le_sInf fun J hJ ↦ ?_)

Premises used: le_antisymm, sInf_le, le_sInf
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
refine_1 :
  Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) (Ideal.map (F := R →+* A) (algebraMap R A) q)
refine_2 :
  ∀ (J : Ideal A) (hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J),
    Ideal.map (F := R →+* A) (algebraMap R A) q ≤ J
⊢ Eq.{u_2 + 1} (α := Ideal A) (sInf (Ideal.under R ⁻¹' I.minimalPrimes)) (Ideal.map (F := R →+* A) (algebraMap R A) q)

Tactic:
refine le_antisymm (sInf_le ?_) (le_sInf fun J hJ ↦ ?_)

Premises used: le_antisymm, sInf_le, le_sInf
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
refine_1 : Ideal.under.{u_1, u_2} R (B := A) (Ideal.map (F := R →+* A) (algebraMap R A) q) ∈ I.minimalPrimes
refine_1₁ : Ideal.under R (IsLocalRing.maximalIdeal A) ∈ I.minimalPrimes
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : q ∈ I.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) (Ideal.map (F := R →+* A) (algebraMap R A) q)

Tactic:
rwa [Set.mem_preimage, map_eq_maximalIdeal q A, under_maximalIdeal A q]

Premises used: IsLocalization.AtPrime.map_eq_maximalIdeal, IsLocalization.AtPrime.isLocalRing, IsLocalization.AtPrime.under_maximalIdeal, Set.mem_preimage
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
refine_2 : q ≤ Ideal.under R J
⊢ Ideal.map (F := R →+* A) (algebraMap R A) q ≤ J

Tactic:
rw [← IsLocalization.under_le_under_iff q.primeCompl A,
      AtPrime.map_eq_maximalIdeal q A, AtPrime.under_maximalIdeal A q]

Premises used: IsLocalization.AtPrime.map_eq_maximalIdeal, IsLocalization.AtPrime.isLocalRing, Ideal.primeCompl, IsLocalization.AtPrime.under_maximalIdeal, IsLocalization.under_le_under_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
refine_2 : Ideal.under R J ≤ q
⊢ q ≤ Ideal.under R J

Tactic:
apply hIq.2 hJ.1

Premises used: And.right, And.left
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
⊢ Ne (α := Ideal R) (Ideal.under R J) ⊤

Tactic:
have := hJ.isPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this_1 : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
this : Ne (α := Ideal R) (Ideal.under R J) ⊤
⊢ Disjoint (↑q.primeCompl : Set R) (↑(Ideal.under R J) : Set R)

Tactic:
rw [ne_eq, Ideal.comap_eq_top_iff, ← ne_eq, ← disjoint_under_iff q.primeCompl A J] at this

Premises used: Ideal.comap_eq_top_iff, ne_eq, Ideal.primeCompl, IsLocalization.disjoint_under_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this_1 : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
this : Disjoint (↑q.primeCompl : Set R) (↑(Ideal.under R J) : Set R)
⊢ Ideal.under R J ≤ q

Tactic:
Set.disjoint_compl_left_iff_subset.mp this

Premises used: Set.disjoint_compl_left_iff_subset, Set.Subset, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this_1 : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
this : Disjoint (↑q.primeCompl : Set R) (↑(Ideal.under R J) : Set R)
⊢ Ideal.under R J ≤ q

Tactic:
exact Set.disjoint_compl_left_iff_subset.mp this

Premises used: Set.disjoint_compl_left_iff_subset, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : Field K
inst_6 : Field L
inst_7 : Field L₂
inst_8 : Algebra A K
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : Algebra K L₂
inst_13 : Algebra A L₂
inst_14 : IsScalarTower A K L₂
inst_15 : Algebra B L
inst_16 : IsScalarTower A B L
inst_17 : IsIntegralClosure B A L
inst_18 : Algebra B₂ L₂
inst_19 : IsScalarTower A B₂ L₂
inst_20 : IsIntegralClosure B₂ A L₂
σ : L →ₐ[K] L₂
x : B
⊢ Eq.{u_4 + 1} (α := L₂) ((algebraMap B₂ L₂ : (a : B₂) → L₂) ((galRestrict' A B B₂ σ : (a : B) → B₂) x : B₂) : L₂)
    ((σ : (a : L) → L₂) ((algebraMap B L : (a : B) → L) x : L) : L₂)

Tactic:
simp [galRestrict', galRestrict', Subalgebra.algebraMap_eq]

Premises used: galRestrict', Subalgebra.algebraMap_eq
-- 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 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra B L
inst_10 : IsScalarTower A B L
inst_11 : IsIntegralClosure B A L
H :
  ∀ (x : B),
    Eq (α := B) ((galRestrict' A B B (AlgHom.id K L) : (a : B) → B) x : B) ((AlgHom.id A B : (a : B) → B) x : B)
⊢ Eq (α := B →ₐ[A] B) (galRestrict' A B B (AlgHom.id K L)) (AlgHom.id A 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 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra B L
inst_10 : IsScalarTower A B L
inst_11 : IsIntegralClosure B A L
x : B
H :
  Eq.{u_3 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((galRestrict' A B B (AlgHom.id K L) : (a : B) → B) x : B) : L)
    ((algebraMap B L : (a : B) → L) ((AlgHom.id A B : (a : B) → B) x : B) : L)
⊢ Eq (α := B) ((galRestrict' A B B (AlgHom.id K L) : (a : B) → B) x : B) ((AlgHom.id A B : (a : B) → B) x : B)

Tactic:
apply IsIntegralClosure.algebraMap_injective B A L

Premises used: IsIntegralClosure.algebraMap_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 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra B L
inst_10 : IsScalarTower A B L
inst_11 : IsIntegralClosure B A L
x : B
⊢ Eq.{u_3 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((galRestrict' A B B (AlgHom.id K L) : (a : B) → B) x : B) : L)
    ((algebraMap B L : (a : B) → L) ((AlgHom.id A B : (a : B) → B) x : B) : L)

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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₃
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₃)
⊢ Eq (α := B →ₐ[A] B₃) (galRestrict' A B B₃ (σ'.comp σ)) (AlgHom.comp (galRestrict' A B₂ B₃ σ') (galRestrict' A B B₂ σ))

Tactic:
ext x
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
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₃))
⊢ 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:
apply (IsIntegralClosure.equiv A (integralClosure A L₃) L₃ B₃).symm.injective

Premises used: IsIntegralClosure.equiv, AlgEquiv.symm, Membership.mem, Subtype, integralClosure, AlgEquiv.injective
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
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₃)
⊢ 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:
ext
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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} (α := 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:
simp [galRestrict', Subalgebra.algebraMap_eq]

Premises used: galRestrict', Subalgebra.algebraMap_eq
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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
x : A
hx : x ∈ (↑(A⁰ : Submonoid A) : Set A)
⊢ IsUnit.{u_4} (M := L₂)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B₂ L₂) (↑σ : B →+* B₂) : (a : B) → L₂)
        ((↑(Subtype.mk (p := fun (x : B) ↦
                Membership.mem (γ := Submonoid B) (Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) x)
                ((algebraMap A B : (a : A) → B) x) ⋯) :
            B) :
          B) :
      L₂)

Tactic:
simpa only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgHom.commutes,
      isUnit_iff_ne_zero, ne_eq, map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective _ _),
      ← IsScalarTower.algebraMap_apply] using nonZeroDivisors.ne_zero hx

Premises used: RingHom.coe_coe, nonZeroDivisors.ne_zero, isUnit_iff_ne_zero, ne_eq, map_eq_zero_iff, FaithfulSMul.algebraMap_injective, AlgHom.commutes, RingHom.coe_comp, Function.comp_apply, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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₂)
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))
⊢ Eq (α := K →+* L₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.lift H) (algebraMap K L))
    (algebraMap K L₂)

Tactic:
apply IsLocalization.ringHom_ext A⁰

Premises used: nonZeroDivisors, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
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₂)
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₂)
⊢ 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:
ext