-- 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_5 :
  Eq (α :=
    HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
      (Ideal.span
        (singleton (α := Localization.Away P.g)
          ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
            Localization.Away P.g))))
    (((AlgHom.comp (B := Localization (Submonoid.powers P.g))
              (AlgHom.comp (B :=
                HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                  (Ideal.span
                    (singleton (α := Localization.Away P.g)
                      ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                        Localization.Away P.g))))
                (AlgHom.comp
                  (P.lift
                    ((algebraMap R[X]
                          (HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                            (Ideal.span
                              (singleton (α := Localization.Away P.g)
                                ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                                  Localization.Away P.g)))) :
                        (a : R[X]) →
                          Localization.Away P.g ⧸
                            Ideal.span
                              {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
                      X)
                    ⋯)
                  (Ideal.Quotient.liftₐ
                    (Ideal.span
                      (singleton (α := Localization.Away P.g)
                        ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                          Localization.Away P.g)))
                    (IsLocalization.liftAlgHom (R := R[X]) (M := Submonoid.powers P.g) (f := aeval P.X) ⋯) ⋯))
                (Ideal.Quotient.mkₐ R
                  (Ideal.span
                    (singleton (α := Localization.Away P.g)
                      ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                        Localization.Away P.g)))))
              (Algebra.algHom R R[X] (Localization (Submonoid.powers P.g))) :
            R[X] →ₐ[R]
              HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                (Ideal.span
                  (singleton (α := Localization.Away P.g)
                    ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                      Localization.Away P.g)))) :
          (a : R[X]) →
            Localization.Away P.g ⧸
              Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
        X :
      HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
        (Ideal.span
          (singleton (α := Localization.Away P.g)
            ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
              Localization.Away P.g))))
    ((AlgHom.comp
            (AlgHom.comp
              (AlgHom.id R
                (HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                  (Ideal.span
                    (singleton (α := Localization.Away P.g)
                      ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                        Localization.Away P.g)))))
              (Ideal.Quotient.mkₐ R
                (Ideal.span
                  (singleton (α := Localization.Away P.g)
                    ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                      Localization.Away P.g)))))
            (Algebra.algHom R R[X] (Localization (Submonoid.powers P.g))) :
          (a : R[X]) →
            Localization.Away P.g ⧸
              Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
        X :
      HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
        (Ideal.span
          (singleton (α := Localization.Away P.g)
            ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
              Localization.Away P.g))))
⊢ Eq (α :=
    Localization.Away P.g →ₐ[R]
      HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
        (Ideal.span
          (singleton (α := Localization.Away P.g)
            ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
              Localization.Away P.g))))
    (AlgHom.comp (B :=
        HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
          (Ideal.span
            (singleton (α := Localization.Away P.g)
              ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                Localization.Away P.g))))
        (AlgHom.comp
          (P.lift
            ((algebraMap R[X]
                  (HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
                    (Ideal.span
                      (singleton (α := Localization.Away P.g)
                        ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                          Localization.Away P.g)))) :
                (a : R[X]) →
                  Localization.Away P.g ⧸
                    Ideal.span {(algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f})
              X)
            ⋯)
          (Ideal.Quotient.liftₐ
            (Ideal.span
              (singleton (α := Localization.Away P.g)
                ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                  Localization.Away P.g)))
            (IsLocalization.liftAlgHom (R := R[X]) (M := Submonoid.powers P.g) (f := aeval P.X) ⋯) ⋯))
        (Ideal.Quotient.mkₐ R
          (Ideal.span
            (singleton (α := Localization.Away P.g)
              ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                Localization.Away P.g)))) :
      Localization.Away P.g →ₐ[R]
        HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
          (Ideal.span
            (singleton (α := Localization.Away P.g)
              ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                Localization.Away P.g))))
    (AlgHom.comp
        (AlgHom.id R
          (HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
            (Ideal.span
              (singleton (α := Localization.Away P.g)
                ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                  Localization.Away P.g)))))
        (Ideal.Quotient.mkₐ R
          (Ideal.span
            (singleton (α := Localization.Away P.g)
              ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                Localization.Away P.g)))) :
      Localization.Away P.g →ₐ[R]
        HasQuotient.Quotient (Localization.Away P.g) (B := Ideal (Localization.Away P.g))
          (Ideal.span
            (singleton (α := Localization.Away P.g)
              ((algebraMap R[X] (Localization.Away P.g) : (a : R[X]) → Localization.Away P.g) P.f :
                Localization.Away P.g))))

Tactic:
ext