-- 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
P : StandardEtalePresentation R S
x : Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
obtain :
  ∀ (p : AdjoinRoot P.f) (n : ℕ)
    (e :
      HMul.hMul (β :=
          Localization.Away (M := AdjoinRoot P.f)
            ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
          x
          ((algebraMap (AdjoinRoot P.f)
                  (Localization.Away (M := AdjoinRoot P.f)
                    ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
                (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
              (↑(p,
                      Subtype.mk (p := fun (x : AdjoinRoot P.f) ↦
                        Membership.mem (γ := Submonoid (AdjoinRoot P.f))
                          (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                            Submonoid (AdjoinRoot P.f))
                          x)
                        ((fun (x : ℕ) ↦
                            HPow.hPow (α := AdjoinRoot P.f)
                              ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) x)
                          n)
                        ⋯).2 :
                AdjoinRoot P.f) :
            Localization.Away (M := AdjoinRoot P.f)
              ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) =
        (algebraMap (AdjoinRoot P.f)
              (Localization.Away (M := AdjoinRoot P.f)
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
            (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
          (p,
              Subtype.mk (p := fun (x : AdjoinRoot P.f) ↦
                Membership.mem (γ := Submonoid (AdjoinRoot P.f))
                  (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                    Submonoid (AdjoinRoot P.f))
                  x)
                ((fun (x : ℕ) ↦
                    HPow.hPow (α := AdjoinRoot P.f)
                      ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) x)
                  n)
                ⋯).1),
    ∃ (p : R[X]) (n : ℕ),
      HMul.hMul (α := S)
          (((P.equivRing.trans P.equivAwayAdjoinRoot).symm :
                (a : Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) → S)
              x :
            S)
          (HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n) =
        (aeval P.x : (a : R[X]) → S) p
⊢ ∃ (p : R[X]) (n : ℕ),
    HMul.hMul (α := S)
        (((P.equivRing.trans P.equivAwayAdjoinRoot).symm :
              (a : Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) → S)
            x :
          S)
        (HPow.hPow (α := S) ((aeval P.x : (a : R[X]) → S) P.g : S) n) =
      (aeval P.x : (a : R[X]) → S) p

Tactic:
obtain ⟨⟨p, ⟨_, n, rfl⟩⟩, e⟩ := IsLocalization.surj (.powers (AdjoinRoot.mk P.f P.g)) x

Premises used: IsLocalization.surj, StandardEtalePresentation.P, StandardEtalePair.f, AdjoinRoot.mk, Submonoid.powers, StandardEtalePair.g, DFunLike.coe, rfl