-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
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)
⊢ 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)
have 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)
Tactic: change f.toMonoidHom (Ideal.Quotient.mk _ .X) = g.toMonoidHom (Ideal.Quotient.mk _ .X)