-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
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
⊢ ∃ (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
have 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)
                        sorry) :
                    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)
              sorry).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
Tactic: obtain ⟨p, rfl⟩ := AdjoinRoot.mk_surjective p
Cleared hypotheses: p, e