-- 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')))
r : R
⊢ Equiv.toFun (α :=
      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'))
      (RingEquiv.toEquiv
          (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) :
        Equiv.{u_1 + 1, u_4 + 1}
          (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ₛ)
      ((algebraMap 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')) :
            (a : R) →
              Localization.Away
                ((algebraMap (AdjoinRoot P.f) S' : (a : AdjoinRoot P.f) → S')
                  ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) p)))
          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')) =
    (algebraMap R Sₛ : (a : R) → Sₛ) r

Tactic:
simp [IsScalarTower.algebraMap_apply R S' (Localization.Away _),
          - AlgEquiv.symm_toRingEquiv, IsScalarTower.algebraMap_eq R S Sₛ]

Premises used: Localization.Away, IsScalarTower.algebraMap_eq, AlgEquiv.symm_toRingEquiv, IsScalarTower.algebraMap_apply