awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B_1 : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B_1
inst_4 : Algebra R B_1
B : Type u_4
inst_5 : CommRing B
inst_6 : Algebra R B
x : S
y : ↥(integralClosure R B)
h :
  ((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
          TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
        (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
      (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := S ⊗[R] B) x ((Algebra.TensorProduct.includeRight : (a : B) → S ⊗[R] B) (↑y : B) : S ⊗[R] B)
⊢ Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        (x ⊗ₜ[R] y) :
      S ⊗[R] B)

Tactic:
convert!
      ((y.2.map (Algebra.TensorProduct.includeRight (R := R) (A := S))).tower_top (A := S)).smul x

Premises used: IsIntegral.smul, IsIntegral.map, IsIntegral.tower_top, Subtype.property, Algebra.TensorProduct.includeRight
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B_1 : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B_1
inst_4 : Algebra R B_1
B : Type u_4
inst_5 : CommRing B
inst_6 : Algebra R B
x : S
y : ↥(integralClosure R B)
⊢ ((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
          TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
        (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
      (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := S ⊗[R] B) x ((Algebra.TensorProduct.includeRight : (a : B) → S ⊗[R] B) (↑y : B) : S ⊗[R] B)

Tactic:
simp [smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B_1 : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B_1
inst_4 : Algebra R B_1
B : Type u_4
inst_5 : CommRing B
inst_6 : Algebra R B
x : TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B)
zero :
  Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
          TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
        (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
      0)
add :
  ∀ (x y : TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B)),
    Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
        (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
                TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
              (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
            x :
          S ⊗[R] B) →
      Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
          (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
                  TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
                (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
              y :
            S ⊗[R] B) →
        Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
          (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
                  TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
                (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
              (x + y) :
            S ⊗[R] B)
tmul :
  ∀ (x : S) (y : ↥(integralClosure R B)),
    Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
      (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
              TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
            (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
          (x ⊗ₜ[R] y) :
        S ⊗[R] B)
⊢ Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        x :
      S ⊗[R] B)

Tactic:
induction x with
  | zero => simp
  | add x y _ _ => rw [map_add]; exact add_mem ‹_› ‹_›
  | tmul x y =>
    convert!
      ((y.2.map (Algebra.TensorProduct.includeRight (R := R) (A := S))).tower_top (A := S)).smul x
    simp [smul_tmul']

Premises used: map_add, TensorProduct.smul_tmul', AddMemClass.add_mem, TensorProduct.tmul
-- 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 : Module.Flat R S
⊢ Function.Injective (α := 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:
Function.Injective.of_comp (f := (integralClosure _ _).val) ?_

Premises used: Set.Mem, setOf, Function.Injective.of_comp
-- 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 : Module.Flat R S
refine :
  Function.Injective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β := S ⊗[R] B)
    (Function.comp (β := ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
      (⇑(Subalgebra.val (integralClosure S (S ⊗[R] B)) :
            ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) →ₐ[S] S ⊗[R] B) :
        (a : ↥(integralClosure S (S ⊗[R] B))) → S ⊗[R] B)
      (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B))))
⊢ Function.Injective (α := 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:
refine Function.Injective.of_comp (f := (integralClosure _ _).val) ?_

Premises used: Function.Injective.of_comp
-- 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 : Module.Flat R S
⊢ Function.Injective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β := S ⊗[R] B)
    (⇑(Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
          TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
      (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)

Tactic:
Module.Flat.lTensor_preserves_injective_linearMap (M := S)
    (integralClosure R B).val.toLinearMap Subtype.val_injective

Premises used: AlgHom.toLinearMap, Module.Flat.lTensor_preserves_injective_linearMap, Quotient.liftOn', Set.Mem, Subtype.val_injective, AddCon.liftOn, Subalgebra.val, integralClosure, TensorProduct, TensorProduct.tmul, AddCon.toQuotient
-- 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 : Module.Flat R S
⊢ Function.Injective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β := S ⊗[R] B)
    (⇑(Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
          TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
      (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)

Tactic:
exact Module.Flat.lTensor_preserves_injective_linearMap (M := S)
    (integralClosure R B).val.toLinearMap Subtype.val_injective

Premises used: AlgHom.toLinearMap, Module.Flat.lTensor_preserves_injective_linearMap, Subtype.val_injective, Subalgebra.val, integralClosure
-- 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
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
H :
  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)))
H' :
  Function.Bijective (α := T ⊗[S] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (β :=
    ↥(integralClosure T (T ⊗[S] (S ⊗[R] B)) : Subalgebra T (T ⊗[S] (S ⊗[R] B))))
    (⇑(toIntegralClosure S T (S ⊗[R] B)) :
      (a : T ⊗[S] ↥(integralClosure S (S ⊗[R] B))) → ↥(integralClosure T (T ⊗[S] (S ⊗[R] B))))
e : TensorProduct.{u_1, u_4, u_3} R T ↥(integralClosure R B) ≃ₐ[T] ↥(integralClosure T (T ⊗[R] B)) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Function.Bijective (α := TensorProduct.{u_1, u_4, u_3} R T ↥(integralClosure R B)) (β :=
    ↥(integralClosure T (T ⊗[R] B))) (⇑e : (a : T ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure T (T ⊗[R] B)))

Tactic:
e.bijective

Premises used: 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
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
H :
  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)))
H' :
  Function.Bijective (α := T ⊗[S] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (β :=
    ↥(integralClosure T (T ⊗[S] (S ⊗[R] B)) : Subalgebra T (T ⊗[S] (S ⊗[R] B))))
    (⇑(toIntegralClosure S T (S ⊗[R] B)) :
      (a : T ⊗[S] ↥(integralClosure S (S ⊗[R] B))) → ↥(integralClosure T (T ⊗[S] (S ⊗[R] B))))
e : TensorProduct.{u_1, u_4, u_3} R T ↥(integralClosure R B) ≃ₐ[T] ↥(integralClosure T (T ⊗[R] B)) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h :
  Eq (α :=
    TensorProduct.{u_1, u_4, u_3} R T ↥(integralClosure R B) →
      ↥(integralClosure T (T ⊗[R] B) : Subalgebra T (T ⊗[R] B)))
    (⇑(toIntegralClosure R T B) : (a : T ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure T (T ⊗[R] B)))
    (⇑e : (a : T ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure T (T ⊗[R] B)))
⊢ Function.Bijective (α := TensorProduct.{u_1, u_4, u_3} R T ↥(integralClosure R B)) (β :=
    ↥(integralClosure T (T ⊗[R] B) : Subalgebra T (T ⊗[R] B)))
    (⇑(toIntegralClosure R T B) : (a : T ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure T (T ⊗[R] B)))

Tactic:
convert! e.bijective

Premises used: 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
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
H :
  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)))
H' :
  Function.Bijective (α := T ⊗[S] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (β :=
    ↥(integralClosure T (T ⊗[S] (S ⊗[R] B)) : Subalgebra T (T ⊗[S] (S ⊗[R] B))))
    (⇑(toIntegralClosure S T (S ⊗[R] B)) :
      (a : T ⊗[S] ↥(integralClosure S (S ⊗[R] B))) → ↥(integralClosure T (T ⊗[S] (S ⊗[R] B))))
e : TensorProduct.{u_1, u_4, u_3} R T ↥(integralClosure R B) ≃ₐ[T] ↥(integralClosure T (T ⊗[R] B)) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : toIntegralClosure R T B = (↑e : T ⊗[R] ↥(integralClosure R B) →ₐ[T] ↥(integralClosure T (T ⊗[R] B)))
⊢ Eq (α :=
    TensorProduct.{u_1, u_4, u_3} R T ↥(integralClosure R B) →
      ↥(integralClosure T (T ⊗[R] B) : Subalgebra T (T ⊗[R] B)))
    (⇑(toIntegralClosure R T B) : (a : T ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure T (T ⊗[R] B)))
    (⇑(↑e : T ⊗[R] ↥(integralClosure R B) →ₐ[T] ↥(integralClosure T (T ⊗[R] B))) :
      (a : T ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure T (T ⊗[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
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
H :
  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)))
H' :
  Function.Bijective (α := T ⊗[S] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (β :=
    ↥(integralClosure T (T ⊗[S] (S ⊗[R] B)) : Subalgebra T (T ⊗[S] (S ⊗[R] B))))
    (⇑(toIntegralClosure S T (S ⊗[R] B)) :
      (a : T ⊗[S] ↥(integralClosure S (S ⊗[R] B))) → ↥(integralClosure T (T ⊗[S] (S ⊗[R] B))))
e : TensorProduct.{u_1, u_4, u_3} R T ↥(integralClosure R B) ≃ₐ[T] ↥(integralClosure T (T ⊗[R] B)) :=
  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)
⊢ toIntegralClosure R T B = (↑e : T ⊗[R] ↥(integralClosure R B) →ₐ[T] ↥(integralClosure T (T ⊗[R] B)))

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
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
inst_7 : Algebra S T
inst_8 : IsScalarTower R S T
H :
  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)))
H' :
  Function.Bijective (α := T ⊗[S] ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (β :=
    ↥(integralClosure T (T ⊗[S] (S ⊗[R] B)) : Subalgebra T (T ⊗[S] (S ⊗[R] B))))
    (⇑(toIntegralClosure S T (S ⊗[R] B)) :
      (a : T ⊗[S] ↥(integralClosure S (S ⊗[R] B))) → ↥(integralClosure T (T ⊗[S] (S ⊗[R] B))))
e : TensorProduct.{u_1, u_4, u_3} R T ↥(integralClosure R B) ≃ₐ[T] ↥(integralClosure T (T ⊗[R] B)) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : ↥(integralClosure R B)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [e, 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
x_1 : ↥(integralClosure R B)
x : B
hx : Membership.mem (γ := Subalgebra R B) (integralClosure R B) x
⊢ Membership.mem (α := S ⊗[R] B) (γ := Subalgebra R (S ⊗[R] B))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B)))
    ((AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)) :
          (a : ↥(integralClosure R B)) → S ⊗[R] B)
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) (integralClosure R B) x) x hx) :
      S ⊗[R] B)

Tactic:
.of_comp (f := algebraMap R S) ?_

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem.of_comp, RingHom.IsIntegralElem, IsIntegral
-- 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
x_1 : ↥(integralClosure R B)
x : B
hx : Membership.mem (γ := Subalgebra R B) (integralClosure R B) x
refine :
  RingHom.IsIntegralElem (A := S ⊗[R] B)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (S ⊗[R] B)) (algebraMap R S) : R →+* S ⊗[R] B)
    ((AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)) :
          (a : ↥(integralClosure R B)) → S ⊗[R] B)
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) (integralClosure R B) x) x hx) :
      S ⊗[R] B)
⊢ Membership.mem (α := S ⊗[R] B) (γ := Subalgebra R (S ⊗[R] B))
    (Subalgebra.restrictScalars R (integralClosure S (S ⊗[R] B)))
    ((AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)) :
          (a : ↥(integralClosure R B)) → S ⊗[R] B)
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) (integralClosure R B) x) x hx) :
      S ⊗[R] B)

Tactic:
refine .of_comp (f := algebraMap 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
M : Submonoid R
inst_5 : IsLocalization M S
x_1 : ↥(integralClosure R B)
x : B
hx : Membership.mem (γ := Subalgebra R B) (integralClosure R B) x
⊢ RingHom.IsIntegralElem (R := R) (A := S ⊗[R] B)
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap R B) : R →+* S ⊗[R] B)
    ((AlgHom.toRingHom Algebra.TensorProduct.includeRight : (a : B) → S ⊗[R] B) x : S ⊗[R] B)

Tactic:
RingHom.IsIntegralElem.map hx
        (Algebra.TensorProduct.includeRight : B →ₐ[R] S ⊗[R] B).toRingHom

Premises used: RingHom.IsIntegralElem.map, AlgHom.toRingHom, Algebra.TensorProduct.includeRight
-- 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
x_1 : ↥(integralClosure R B)
x : B
hx : Membership.mem (γ := Subalgebra R B) (integralClosure R B) x
h :
  Eq (α := R →+* S ⊗[R] B)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (S ⊗[R] B)) (algebraMap R S))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap R B))
⊢ RingHom.IsIntegralElem (A := S ⊗[R] B)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (S ⊗[R] B)) (algebraMap R S) : R →+* S ⊗[R] B)
    ((AlgHom.comp Algebra.TensorProduct.includeRight (Subalgebra.val (integralClosure R B)) :
          (a : ↥(integralClosure R B)) → S ⊗[R] B)
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) (integralClosure R B) x) x hx) :
      S ⊗[R] B)

Tactic:
convert!
      RingHom.IsIntegralElem.map hx
        (Algebra.TensorProduct.includeRight : B →ₐ[R] S ⊗[R] B).toRingHom

Premises used: RingHom.IsIntegralElem.map, AlgHom.toRingHom, Algebra.TensorProduct.includeRight
-- 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
x_1 : ↥(integralClosure R B)
x : B
hx : Membership.mem (γ := Subalgebra R B) (integralClosure R B) x
⊢ Eq (α := R →+* S ⊗[R] B)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (S ⊗[R] B)) (algebraMap R S))
    (RingHom.comp (AlgHom.toRingHom Algebra.TensorProduct.includeRight) (algebraMap R B))

Tactic:
simp [← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq
-- 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 : Algebra ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) := φ.toAlgebra
⊢ IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))

Tactic:
have := IsScalarTower.of_algebraMap_eq' φ.comp_algebraMap.symm
-- 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 : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
⊢ IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)

Tactic:
have : IsScalarTower (integralClosure R B) (integralClosure S (S ⊗[R] B)) (S ⊗[R] B) :=
    .of_algebraMap_eq' 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
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 : IsScalarTower (↥(integralClosure R B)) (↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))) (S ⊗[R] B)
⊢ IsLocalization (R := ↥(integralClosure R B)) (Algebra.algebraMapSubmonoid (↥(integralClosure R B)) M)
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))

Tactic:
have := IsLocalization.integralClosure (S := B) M (Rf := S) (Sf := S ⊗[R] B)