awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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)
⊢ 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)
have 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)
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']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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)
⊢ 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)
have 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)
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']
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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)))
have 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))))
Tactic: refine Function.Injective.of_comp (f := (integralClosure _ _).val) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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) : Subalgebra T (T ⊗[R] B)))
    (⇑(toIntegralClosure R T B) : (a : T ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure T (T ⊗[R] B)))
have 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)))
Tactic: convert! e.bijective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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)
⊢ 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)))
have h : toIntegralClosure R T B = (↑e : T ⊗[R] ↥(integralClosure R B) →ₐ[T] ↥(integralClosure T (T ⊗[R] B)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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)
⊢ toIntegralClosure R T B = (↑e : T ⊗[R] ↥(integralClosure R B) →ₐ[T] ↥(integralClosure T (T ⊗[R] B)))
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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)
have 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)
Tactic: refine .of_comp (f := algebraMap R S) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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 (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)
have 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))
Tactic: convert!
      RingHom.IsIntegralElem.map hx
        (Algebra.TensorProduct.includeRight : B →ₐ[R] S ⊗[R] B).toRingHom
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (hypothesis)
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
⊢ 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)))
have this₁ : IsScalarTower R ↥(integralClosure R B) ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B))
Tactic: have := IsScalarTower.of_algebraMap_eq' φ.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (hypothesis)
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))
⊢ 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)))
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (hypothesis)
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)
⊢ 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)))
have this₁ : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
have 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)))
Tactic: convert!
    (IsLocalization.algEquiv (Algebra.algebraMapSubmonoid (integralClosure R B) M)
        (S ⊗[R] integralClosure R B) (integralClosure S (S ⊗[R] B))).bijective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
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))
⊢ 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)))
have 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)))
Tactic: rw [← AlgHom.coe_restrictScalars' R, ← AlgEquiv.coe_restrictScalars' R, ← AlgEquiv.coe_algHom]