-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
P : StandardEtalePair R
refine_1 :
  Eq (α :=
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (((aeval
              ((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.root P.f)) :
            R[X] →ₐ[R]
              Localization.Away (M := AdjoinRoot P.f)
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
          (a : R[X]) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
        P.f :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (0 :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
refine_2 :
  IsUnit (M :=
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
    (((aeval
              ((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.root P.f)) :
            R[X] →ₐ[R]
              Localization.Away (M := AdjoinRoot P.f)
                ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
          (a : R[X]) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
        P.g :
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
refine_3 :
  ∀ (a : AdjoinRoot P.f)
    (b :
      Membership.mem (γ := Submonoid (AdjoinRoot P.f))
        (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) : Submonoid (AdjoinRoot P.f)) a),
    IsUnit (M := P.Ring)
      ((AdjoinRoot.liftAlgHom P.f (Algebra.ofId R P.Ring) P.X ⋯ : (a : AdjoinRoot P.f) → P.Ring)
          (↑(Subtype.mk (p := fun (a : 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))
                  a)
                a b) :
            AdjoinRoot P.f) :
        P.Ring)
⊢ P.Ring ≃ₐ[R]
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)
have refine_4 : Eq (α :=
  Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) →ₐ[R]
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
  (AlgHom.comp (B := P.Ring)
      (P.lift
        ((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.root P.f))
        sorry)
      (IsLocalization.liftAlgHom (R := AdjoinRoot P.f) (M :=
        Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)) (f :=
        AdjoinRoot.liftAlgHom P.f (Algebra.ofId R P.Ring) P.X sorry) sorry) :
    Localization.Away (M := AdjoinRoot P.f)
        ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) →ₐ[R]
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
  (AlgHom.id R
      (Localization.Away (M := AdjoinRoot P.f)
        ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)) :
    Localization.Away (M := AdjoinRoot P.f)
        ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) →ₐ[R]
      Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
Tactic: refine .ofAlgHom (P.lift (algebraMap (AdjoinRoot P.f) _ (.root P.f)) ⟨?_, ?_⟩)
    (IsLocalization.liftAlgHom (M := .powers <| AdjoinRoot.mk P.f P.g)
      (f := AdjoinRoot.liftAlgHom _ _ P.X P.hasMap_X.1) <| Subtype.forall.mpr ?_) ?_ ?_