-- Module: Mathlib.RingTheory.Etale.StandardEtale
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_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))
                  ⋯)
                (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 ⋯) ⋯))
              (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))
⊢ 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))

Tactic:
ext