-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsStandardEtale R S
Sₛ : Type u_4
inst_4 : CommRing Sₛ
inst_5 : Algebra S Sₛ
inst_6 : Algebra R Sₛ
inst_7 : IsScalarTower R S Sₛ
s : S
inst_8 : IsLocalization.Away s Sₛ
P : StandardEtalePresentation R S
p : R[X]
n : ℕ
hp : s * HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n = (aeval P.x : (a : R[X]) → S) p
P' : StandardEtalePair R := { f := P.f, monic_f := ⋯, g := p * P.g, cond := ⋯ }
S' : Type u_1 :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
e : S ≃ₐ[R] S' := P.equivRing.trans P.equivAwayAdjoinRoot
this_1 :
  IsLocalization.Away (R := AdjoinRoot P.f)
    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g) : AdjoinRoot P.f)
    (Localization.Away (M := S')
      ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
        S'))
H :
  Eq (α := Submonoid S)
    (Submonoid.map (M := S') e.symm.toRingEquiv.toMonoidHom
      (Submonoid.powers
          ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p)) :
        Submonoid S'))
    (Submonoid.powers ((aeval P.x : (a : R[X]) → S) p))
this : IsLocalization.Away.{u_2, u_4} (R := S) ((aeval P.x : (a : R[X]) → S) p : S) Sₛ
e₁ : P'.Ring ≃ₐ[R]
  Localization.Away (M := S')
    ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
        ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
      S') :=
  P'.equivAwayAdjoinRoot.trans
    (AlgEquiv.restrictScalars R (S := AdjoinRoot P.f)
      (IsLocalization.algEquiv (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g)))
          (Localization.Away (M := AdjoinRoot P.f)
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g) : AdjoinRoot P.f))
          (Localization.Away (M := S')
            ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
              S')) :
        Localization.Away (M := AdjoinRoot P.f)
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) (p * P.g) : AdjoinRoot P.f) ≃ₐ[AdjoinRoot P.f]
          Localization.Away (M := S')
            ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
              S')))
e₂ : Localization.Away (M := S')
    ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
        ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
      S') ≃ₐ[R]
  Sₛ :=
  let __spread.0 :
    RingEquiv.{u_1, u_4}
      (Localization.Away (M := S')
        ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
          S'))
      Sₛ :=
    IsLocalization.ringEquivOfRingEquiv
      (Localization.Away (M := S')
        ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p) :
          S'))
      Sₛ e.symm.toRingEquiv H;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ IsStandardEtale R Sₛ

Tactic:
exact .of_equiv (e₁.trans e₂)