-- 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)
                ⋯)))))
hfg : IsIntegral R (A := AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)
heg :
  ∀ (g : R[X]),
    Eq.{u_3 + 1} (α :=
      Localization.Away (M := AdjoinRoot 𝓟'.f)
        ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
      ((e : (a : B ⊗[R] S) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
          (1 ⊗ₜ[R] (aeval 𝓟.x : (a : R[X]) → S) g) :
        Localization.Away (M := AdjoinRoot 𝓟'.f)
          ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
      ((algebraMap (AdjoinRoot 𝓟'.f)
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)) :
            (a : AdjoinRoot 𝓟'.f) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
          ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) (Polynomial.map (algebraMap R B) g)) :
        Localization.Away (M := AdjoinRoot 𝓟'.f)
          ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
k : ℕ
hk :
  IsIntegral R
    (HPow.hPow (α := AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) k *
      a)
y : B[X]
hy :
  HMul.hMul (α := AdjoinRoot 𝓟'.f)
      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) ((derivative : (a : B[X]) → B[X]) 𝓟'.f) : AdjoinRoot 𝓟'.f)
      (HPow.hPow (α := AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) k *
        a) =
    (AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) y
hRy : ∀ (i : ℕ), IsIntegral R (y.coeff i)
h :
  (algebraMap (AdjoinRoot 𝓟'.f)
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)) :
            (a : AdjoinRoot 𝓟'.f) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
          ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f)
            (Polynomial.map (algebraMap R B) ((derivative : (a : R[X]) → R[X]) 𝓟.f))) *
        (HPow.hPow (α :=
            Localization.Away (M := AdjoinRoot 𝓟'.f)
              ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
            ((algebraMap (AdjoinRoot 𝓟'.f)
                  (Localization.Away (M := AdjoinRoot 𝓟'.f)
                    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)) :
                (a : AdjoinRoot 𝓟'.f) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
              ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) (Polynomial.map (algebraMap R B) 𝓟.g)))
            k *
          HPow.hPow (α :=
            Localization.Away (M := AdjoinRoot 𝓟'.f)
              ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
            ((algebraMap (AdjoinRoot 𝓟'.f)
                  (Localization.Away (M := AdjoinRoot 𝓟'.f)
                    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)) :
                (a : AdjoinRoot 𝓟'.f) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
              ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) (Polynomial.map (algebraMap R B) 𝓟.g)))
            m) *
      IsLocalization.mk' (M := Submonoid.powers ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
        (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)
          (HPow.hPow (α := AdjoinRoot 𝓟'.f) ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)
            m)
          ⋯) =
    HMul.hMul (α :=
      Localization.Away (M := AdjoinRoot 𝓟'.f)
        ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
      ((algebraMap (AdjoinRoot 𝓟'.f)
              (Localization.Away (M := AdjoinRoot 𝓟'.f)
                ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)) :
            (a : AdjoinRoot 𝓟'.f) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
          ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) ((derivative : (a : B[X]) → B[X]) 𝓟'.f)) :
        Localization.Away (M := AdjoinRoot 𝓟'.f)
          ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
      (HMul.hMul (β :=
        Localization.Away (M := AdjoinRoot 𝓟'.f)
          ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
        (HPow.hPow (α :=
          Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          ((algebraMap (AdjoinRoot 𝓟'.f)
                  (Localization.Away (M := AdjoinRoot 𝓟'.f)
                    ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)) :
                (a : AdjoinRoot 𝓟'.f) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
              ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g) :
            Localization.Away (M := AdjoinRoot 𝓟'.f)
              ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
          k)
        ((algebraMap (AdjoinRoot 𝓟'.f)
                (Localization.Away (M := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)) :
              (a : AdjoinRoot 𝓟'.f) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
            a :
          Localization.Away (M := AdjoinRoot 𝓟'.f)
            ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)))
⊢ Eq.{u_3 + 1} (α :=
    Localization.Away (M := AdjoinRoot 𝓟'.f)
      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
    ((e : (a : B ⊗[R] S) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
        ((AlgEquiv.symm (Algebra.TensorProduct.comm R B S) : (a : S ⊗[R] B) → B ⊗[R] S)
          (HSMul.hSMul (β := S ⊗[R] B)
            (HMul.hMul (α := S) ((aeval 𝓟.x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) 𝓟.f : R[X]) : S)
              (HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) k *
                HPow.hPow (α := S) ((aeval 𝓟.x : (a : R[X]) → S) 𝓟.g : S) 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)
                (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)
                    ⋯)))))) :
      Localization.Away (M := AdjoinRoot 𝓟'.f)
        ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))
    ((e : (a : B ⊗[R] S) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
        ((AlgEquiv.symm (Algebra.TensorProduct.comm R B S) : (a : S ⊗[R] B) → B ⊗[R] S)
          ((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)
              ((algebraMap (AdjoinRoot 𝓟'.f)
                    (Localization.Away (M := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f)) :
                  (a : AdjoinRoot 𝓟'.f) → Localization.Away ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g))
                (HMul.hMul (α := AdjoinRoot 𝓟'.f)
                  ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) ((derivative : (a : B[X]) → B[X]) 𝓟'.f) :
                    AdjoinRoot 𝓟'.f)
                  (HPow.hPow (α := AdjoinRoot 𝓟'.f)
                      ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f) k *
                    a)))))) :
      Localization.Away (M := AdjoinRoot 𝓟'.f)
        ((AdjoinRoot.mk 𝓟'.f : (a : B[X]) → AdjoinRoot 𝓟'.f) 𝓟'.g : AdjoinRoot 𝓟'.f))

Tactic:
simp only [Algebra.smul_def, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
        RingHom.id_apply, map_mul, Algebra.TensorProduct.comm_symm_tmul, AlgEquiv.symm_apply_apply,
        AlgEquiv.apply_symm_apply, map_pow, heg]

Premises used: Algebra.TensorProduct.algebraMap_apply, RingHom.id_apply, Algebra.algebraMap_self, AlgEquiv.apply_symm_apply, map_pow, map_mul, AlgEquiv.symm_apply_apply, Algebra.TensorProduct.comm_symm_tmul, Algebra.smul_def