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
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)))))
this :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
obtain :
  ∀ (m : ℕ)
    (hm :
      IsIntegral (AdjoinRoot 𝓟.f)
        (Subtype.mk (p := fun (x : AdjoinRoot 𝓟.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)
                  x)
              m)
            ⋯ •
          a)),
    ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)

Tactic:
obtain ⟨⟨_, m, rfl⟩, hm⟩ := IsIntegral.exists_multiple_integral_of_isLocalization
      (R := AdjoinRoot 𝓟.f) (.powers (.mk _ 𝓟.g)) _ hx

Premises used: IsIntegral.exists_multiple_integral_of_isLocalization, StandardEtalePresentation.P, AdjoinRoot.mk, Submonoid.powers, StandardEtalePair.g, DFunLike.coe, 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
𝓟 : 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)))))
this :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
m : ℕ
hm :
  IsIntegral (AdjoinRoot 𝓟.f)
    (Subtype.mk (p := fun (x : AdjoinRoot 𝓟.f) ↦
        Membership.mem (γ := Submonoid (AdjoinRoot 𝓟.f))
          (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) x)
        ((fun (x : ℕ) ↦
            HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) x)
          m)
        ⋯ •
      a)
⊢ ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HMul.hMul (α := S ⊗[R] B)
        ((algebraMap (AdjoinRoot 𝓟.f) (S ⊗[R] B) : (a : AdjoinRoot 𝓟.f) → S ⊗[R] B)
            (HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)
              k) :
          S ⊗[R] B)
        (Subtype.mk (p := fun (x : AdjoinRoot 𝓟.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)
                  x)
              m)
            ⋯ •
          a))

Tactic:
replace hm := fun k : ℕ ↦ (isIntegral_algebraMap (x := AdjoinRoot.mk 𝓟.f 𝓟.g ^ k)).mul hm
-- 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)))))
this :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
m : ℕ
hm :
  ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HMul.hMul (α := S ⊗[R] B)
        ((algebraMap (AdjoinRoot 𝓟.f) (S ⊗[R] B) : (a : AdjoinRoot 𝓟.f) → S ⊗[R] B)
            (HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)
              k) :
          S ⊗[R] B)
        (Subtype.mk (p := fun (x : AdjoinRoot 𝓟.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟.f) ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f)
                  x)
              m)
            ⋯ •
          a))
⊢ ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HSMul.hSMul (α := S)
        ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) (𝓟.g ^ (m + k)) : AdjoinRoot 𝓟.f) :
          S)
        a)

Tactic:
simp only [Submonoid.smul_def, ← @IsScalarTower.algebraMap_smul (AdjoinRoot 𝓟.f) S,
      ← map_pow, ← Algebra.smul_def, ← mul_smul, ← map_mul, ← pow_add, add_comm _ m] at hm

Premises used: pow_add, map_pow, add_comm, Submonoid.smul_def, IsScalarTower.algebraMap_smul, map_mul, Algebra.smul_def, SemigroupAction.mul_smul
-- 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)))))
this :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
m : ℕ
hm :
  ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HSMul.hSMul (α := S)
        ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
            ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) (𝓟.g ^ (m + k)) : AdjoinRoot 𝓟.f) :
          S)
        a)
⊢ ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HPow.hPow (α := S)
          ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
              ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :
            S)
          (m + k) •
        a)

Tactic:
simp_rw [map_pow] at hm

Premises used: map_pow
-- 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)))))
this :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
m : ℕ
hm :
  ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HPow.hPow (α := S)
          ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
              ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :
            S)
          (m + k) •
        a)
⊢ Module.Finite R (AdjoinRoot 𝓟.f)

Tactic:
have := 𝓟.monic_f.finite_adjoinRoot
-- 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)))))
this_1 :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
m : ℕ
hm :
  ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HPow.hPow (α := S)
          ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
              ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :
            S)
          (m + k) •
        a)
this : Module.Finite R (AdjoinRoot 𝓟.f)
suffices :
  Eq.{u_2 + 1} (α := S)
    ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
        ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :
      S)
    ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)

Tactic:
suffices algebraMap (AdjoinRoot 𝓟.f) S (.mk _ 𝓟.g) = aeval 𝓟.x 𝓟.g from
      ⟨m, fun k ↦ this ▸ isIntegral_trans (R := R) _ (hm k)⟩
-- 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)))))
this_1 :
  IsLocalization (R := AdjoinRoot 𝓟.f)
    (Submonoid.powers ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g) : Submonoid (AdjoinRoot 𝓟.f)) S
m : ℕ
hm :
  ∀ (k : ℕ),
    IsIntegral (AdjoinRoot 𝓟.f)
      (HPow.hPow (α := S)
          ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
              ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :
            S)
          (m + k) •
        a)
this : Module.Finite R (AdjoinRoot 𝓟.f)
⊢ Eq.{u_2 + 1} (α := S)
    ((algebraMap (AdjoinRoot 𝓟.f) S : (a : AdjoinRoot 𝓟.f) → S)
        ((AdjoinRoot.mk 𝓟.f : (a : R[X]) → AdjoinRoot 𝓟.f) 𝓟.g : AdjoinRoot 𝓟.f) :
      S)
    ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S)

Tactic:
simp [RingHom.algebraMap_toAlgebra, e, StandardEtalePair.equivAwayAdjoinRoot,
      ← aeval_def, ← aeval_algHom_apply]

Premises used: StandardEtalePair.equivAwayAdjoinRoot, Polynomial.aeval_def, RingHom.algebraMap_toAlgebra, Polynomial.aeval_algHom_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
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
obtain :
  ∀ (n : ℕ) (hx : ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)),
    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:
obtain ⟨n, hx⟩ : ∃ n, ∀ m, IsIntegral R ((aeval 𝓟.x 𝓟.g) ^ (n + m) • a) := by
    let e := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
    algebraize [(e.symm.toAlgHom.comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) _)).toRingHom]
    have := IsLocalization.isLocalization_of_algEquiv (R := AdjoinRoot 𝓟.f) (.powers (.mk _ 𝓟.g))
      { toRingEquiv := e.symm.toRingEquiv, commutes' := by simp [RingHom.algebraMap_toAlgebra] }
    obtain ⟨⟨_, m, rfl⟩, hm⟩ := IsIntegral.exists_multiple_integral_of_isLocalization
      (R := AdjoinRoot 𝓟.f) (.powers (.mk _ 𝓟.g)) _ hx
    replace hm := fun k : ℕ ↦ (isIntegral_algebraMap (x := AdjoinRoot.mk 𝓟.f 𝓟.g ^ k)).mul hm
    simp only [Submonoid.smul_def, ← @IsScalarTower.algebraMap_smul (AdjoinRoot 𝓟.f) S,
      ← map_pow, ← Algebra.smul_def, ← mul_smul, ← map_mul, ← pow_add, add_comm _ m] at hm
    simp_rw [map_pow] at hm
    have := 𝓟.monic_f.finite_adjoinRoot
    suffices algebraMap (AdjoinRoot 𝓟.f) S (.mk _ 𝓟.g) = aeval 𝓟.x 𝓟.g from
      ⟨m, fun k ↦ this ▸ isIntegral_trans (R := R) _ (hm k)⟩
    simp [RingHom.algebraMap_toAlgebra, e, StandardEtalePair.equivAwayAdjoinRoot,
      ← aeval_def, ← aeval_algHom_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
inst_5 : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx_1 : IsIntegral S a
𝓟 : StandardEtalePresentation R S
n : ℕ
hx : ∀ (m : ℕ), IsIntegral R (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m) • a)
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
obtain :
  ∀ (a : B ⊗[R] S)
    (hx : IsIntegral S (A := S ⊗[R] B) ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B))
    (hx :
      ∀ (m : ℕ),
        IsIntegral R
          (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m))
            ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B))),
    Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B))
      (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B)))
      ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B)
⊢ Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B))) a

Tactic:
obtain ⟨a, rfl⟩ := (Algebra.TensorProduct.comm _ _ _).surjective a

Premises used: Algebra.TensorProduct.comm, AlgEquiv.surjective, 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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : B ⊗[R] S
hx_1 : IsIntegral S (A := S ⊗[R] B) ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B)
hx :
  ∀ (m : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B))
obtain :
  ∀
    (a :
      Localization.Away (M := AdjoinRoot 𝓟'.f)
        ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
    (hx :
      IsIntegral S (A := S ⊗[R] B)
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
            ((e.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
              a) :
          S ⊗[R] B))
    (hx :
      ∀ (m : ℕ),
        IsIntegral R
          (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m))
            ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
                ((e.symm :
                    (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
                  a) :
              S ⊗[R] B))),
    Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B))
      (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B)))
      ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S) a) :
        S ⊗[R] B)
⊢ Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B))
    (Algebra.adjoin S (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B)))
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B) a : S ⊗[R] B)

Tactic:
obtain ⟨a, rfl⟩ := e.symm.surjective a

Premises used: AlgEquiv.symm, AlgEquiv.surjective, 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
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B]
  Localization.Away (M := AdjoinRoot 𝓟'.f)
    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) :=
  𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx_1 :
  IsIntegral S (A := S ⊗[R] B)
    ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
      ((e.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
        (IsLocalization.mk'
          (Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          a
          (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
            Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
              (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                Submonoid (AdjoinRoot 𝓟'.f))
              x)
            ((fun (x : ℕ) ↦
                HPow.hPow (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
              m)
            ⋯))))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      (HSMul.hSMul (β := S ⊗[R] B) (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) (n + m_1))
        ((Algebra.TensorProduct.comm R B S : (a : B ⊗[R] S) → S ⊗[R] B)
          ((e.symm : (a : Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g)) → B ⊗[R] S)
            (IsLocalization.mk'
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
              a
              (Subtype.mk (p := fun (x : AdjoinRoot 𝓟'.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot 𝓟'.f))
                  (Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
                    Submonoid (AdjoinRoot 𝓟'.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) x)
                  m)
                ⋯)))))
⊢ Module.Finite R (AdjoinRoot 𝓟.f)

Tactic:
have := 𝓟.monic_f.finite_adjoinRoot