-- 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
⊢ 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))
          ⋯)
        (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 ⋯) ⋯) :
      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))
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))
  (((AlgHom.comp (B :=
            Localization (M := AdjoinRoot P.f)
              (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) : Submonoid (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))
            (Algebra.algHom R (AdjoinRoot P.f)
              (Localization (M := AdjoinRoot P.f)
                (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                  Submonoid (AdjoinRoot P.f)))) :
          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)) :
        (a : AdjoinRoot P.f) → Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
      (AdjoinRoot.root P.f) :
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
  ((AlgHom.comp
          (AlgHom.id R
            (Localization.Away (M := AdjoinRoot P.f)
              ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f)))
          (Algebra.algHom R (AdjoinRoot P.f)
            (Localization (M := AdjoinRoot P.f)
              (Submonoid.powers ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g) :
                Submonoid (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) :
    Localization.Away (M := AdjoinRoot P.f) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f))
Tactic: ext