-- 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)
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
obtain :
  ∀ (p : R[X])
    (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))
              (↑(((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) 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)
                          ⋯) :
                      AdjoinRoot P.f ×
                        ↥(Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                            Submonoid (AdjoinRoot P.f))).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))
          ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) 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, rfl⟩ := AdjoinRoot.mk_surjective p

Premises used: AdjoinRoot.mk_surjective, rfl