awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
          (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
          ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) :
      (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))

Tactic:
(IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (integralClosure R B) M)
        (S ⊗[R] integralClosure R B) (integralClosure S (S ⊗[R] B))).bijective

Premises used: Membership.mem, Subtype, integralClosure, IsLocalization.algEquiv, TensorProduct, Algebra.algebraMapSubmonoid, AlgEquiv.bijective
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
h :
  Eq (α :=
    TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
    (⇑(IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
          (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
          ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) :
      (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))

Tactic:
convert!
    (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (integralClosure R B) M)
        (S ⊗[R] integralClosure R B) (integralClosure S (S ⊗[R] B))).bijective

Premises used: Membership.mem, Subtype, integralClosure, IsLocalization.algEquiv, TensorProduct, Algebra.algebraMapSubmonoid, AlgEquiv.bijective
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
h :
  Eq (α :=
    TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(AlgHom.restrictScalars R (toIntegralClosure R S B)) :
      (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
    (⇑((↑(AlgEquiv.restrictScalars R (S := ↥(integralClosure R B))
                (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
                  (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
                  ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))) :
            TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
              ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) :
          TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
            ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) :
      (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
⊢ Eq (α :=
    TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
    (⇑(IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
          (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
          ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) :
      (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))

Tactic:
rw [← AlgHom.coe_restrictScalars' R, ← AlgEquiv.coe_restrictScalars' R, ← AlgEquiv.coe_algHom]

Premises used: AlgEquiv.coe_restrictScalars', AlgHom.coe_restrictScalars', AlgEquiv.coe_algHom
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
h :
  Eq (α :=
    TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (AlgHom.restrictScalars R (toIntegralClosure R S B))
    (↑(AlgEquiv.restrictScalars R (S := ↥(integralClosure R B))
          (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
            (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
            ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))) :
      S ⊗[R] ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)))
⊢ Eq (α :=
    TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(AlgHom.restrictScalars R (toIntegralClosure R S B)) :
      (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
    (⇑((↑(AlgEquiv.restrictScalars R (S := ↥(integralClosure R B))
                (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
                  (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
                  ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))) :
            TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
              ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) :
          TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
            ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) :
      (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α :=
    TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[R]
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (AlgHom.restrictScalars R (toIntegralClosure R S B))
    (↑(AlgEquiv.restrictScalars R (S := ↥(integralClosure R B))
          (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
            (TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
            ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))) :
      S ⊗[R] ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B)))

Tactic:
ext1
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply IsLocalization.algHom_ext M

Premises used: IsLocalization.algHom_ext
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
x : ↥(integralClosure R B)
h :
  Eq (α := S ⊗[R] B) (1 ⊗ₜ[R] (↑x : B))
    (↑((IsLocalization.map (R := ↥(integralClosure R B)) (M := Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
              (T := Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
              (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (RingHom.id ↥(integralClosure R B)) ⋯ :
            (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
          (1 ⊗ₜ[R] x)) :
      S ⊗[R] B)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp [toIntegralClosure]

Premises used: TensorProduct.toIntegralClosure
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
x : ↥(integralClosure R B)
h :
  Eq (α := S ⊗[R] B) ((algebraMap B (S ⊗[R] B) : (a : B) → S ⊗[R] B) (↑x : B) : S ⊗[R] B)
    ((↑((algebraMap ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :
              (a : ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
            x) :
        S ⊗[R] B) :
      S ⊗[R] B)
⊢ Eq (α := S ⊗[R] B) (1 ⊗ₜ[R] (↑x : B))
    (↑((IsLocalization.map (R := ↥(integralClosure R B)) (M := Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
              (T := Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
              (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (RingHom.id ↥(integralClosure R B)) ⋯ :
            (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
          (1 ⊗ₜ[R] x)) :
      S ⊗[R] B)

Tactic:
simp [← Algebra.TensorProduct.right_algebraMap_apply]

Premises used: Algebra.TensorProduct.right_algebraMap_apply
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
M : Submonoid R
inst_5 : IsLocalization M S
φ : ↥(integralClosure R B) →ₐ[R] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :=
  AlgHom.codRestrict (AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B))) ⋯
this_1 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
this_2 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
this_3 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
this :
  IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
x : ↥(integralClosure R B)
⊢ Eq (α := S ⊗[R] B) ((algebraMap B (S ⊗[R] B) : (a : B) → S ⊗[R] B) (↑x : B) : S ⊗[R] B)
    ((↑((algebraMap ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) :
              (a : ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
            x) :
        S ⊗[R] B) :
      S ⊗[R] B)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
have :
  ∀ (𝓟 : StandardEtalePresentation R S),
    Membership.mem (γ := Subalgebra S (S ⊗[R] B))
      (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B))) a
⊢ Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B))) a

Tactic:
have 𝓟 := Classical.ofNonempty (α := StandardEtalePresentation R S)
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R]
  Localization.Away (M := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :=
  𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst : Algebra.{u_1, u_2} (AdjoinRoot 𝓟.f) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      ((↑e.symm : Localization.Away ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) →ₐ[R] S).comp
        (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f)
          (Localization.Away (M := AdjoinRoot 𝓟.f)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)))))
⊢ ∀ (r : AdjoinRoot 𝓟.f),
    e.symm.toRingEquiv.toFun
        ((algebraMap (AdjoinRoot 𝓟.f)
              (Localization.Away (M := AdjoinRoot 𝓟.f)
                ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)) :
            (a : AdjoinRoot 𝓟.f) → Localization.Away ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g))
          r) =
      (algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S) r

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R]
  Localization.Away (M := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :=
  𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst : Algebra.{u_1, u_2} (AdjoinRoot 𝓟.f) S :=
  RingHom.toAlgebra
    (AlgHom.toRingHom
      ((↑e.symm : Localization.Away ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) →ₐ[R] S).comp
        (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f)
          (Localization.Away (M := AdjoinRoot 𝓟.f)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)))))
⊢ IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S

Tactic:
have := IsLocalization.isLocalization_of_algEquiv (R := AdjoinRoot 𝓟.f) (.powers (.mk _ 𝓟.g))
      { toRingEquiv := e.symm.toRingEquiv, commutes' := by simp [RingHom.algebraMap_toAlgebra] }