-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : StandardEtalePair R
f g : P.Ring →ₐ[R] S
H_1 : Eq.{u_2 + 1} (α := S) ((f : (a : P.Ring) → S) P.X : S) ((g : (a : P.Ring) → S) P.X : S)
H :
  (f.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom =
    (g.comp
          (Ideal.Quotient.mkₐ R
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))).comp
      CAlgHom
H' :
  Eq (α := R[X] →ₐ[R] P.Ring) (aeval P.X)
    (AlgHom.comp
      (Ideal.Quotient.mkₐ R
        (Ideal.span
          (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
            {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})))
      CAlgHom)
change :
  Eq.{u_2 + 1} (α := S)
    (((↑f.toRingHom : P.Ring →* S) : (a : P.Ring) → S)
        ((Ideal.Quotient.mk
                (Ideal.span
                  (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                    {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})) :
              (a : R[X][Y]) →
                R[X][Y] ⧸ Ideal.span {(C : (a : R[X]) → R[X][Y]) P.f, Y * (C : (a : R[X]) → R[X][Y]) P.g - 1})
            Y :
          HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1}))) :
      S)
    (((↑g.toRingHom : P.Ring →* S) : (a : P.Ring) → S)
        ((Ideal.Quotient.mk
                (Ideal.span
                  (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                    {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1})) :
              (a : R[X][Y]) →
                R[X][Y] ⧸ Ideal.span {(C : (a : R[X]) → R[X][Y]) P.f, Y * (C : (a : R[X]) → R[X][Y]) P.g - 1})
            Y :
          HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y])
            (Ideal.span
              (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1}))) :
      S)
⊢ Eq.{u_2 + 1} (α := S)
    ((f.comp
            (Ideal.Quotient.mkₐ R
              (Ideal.span
                (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                  {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1}))) :
          (a : R[X][Y]) → S)
        Y :
      S)
    ((g.comp
            (Ideal.Quotient.mkₐ R
              (Ideal.span
                (insert (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.f : R[X][Y])
                  {HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1}))) :
          (a : R[X][Y]) → S)
        Y :
      S)

Tactic:
change f.toMonoidHom (Ideal.Quotient.mk _ .X) = g.toMonoidHom (Ideal.Quotient.mk _ .X)

Premises used: Ideal.Quotient.mk, AlgHom.toRingHom, RingHom.toMonoidHom, Polynomial.X, DFunLike.coe