-- Module: Mathlib.RingTheory.Etale.StandardEtale
Goal:
R : Type u_1
inst : CommRing R
P : StandardEtalePair R
this :
  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)
rw :
  Eq (α :=
    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]) ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) Y - 1})))
    ((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]) ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) Y - 1})) :
          (a : R[X][Y]) → R[X][Y] ⧸ Ideal.span {(C : (a : R[X]) → R[X][Y]) P.f, (C : (a : R[X]) → R[X][Y]) P.g * Y - 1})
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) Y - 1) :
      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]) ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) Y - 1})))
    (0 :
      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]) ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) Y - 1})))
⊢ HMul.hMul (α :=
      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})))
      (β :=
      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})))
      ((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})
          ((C : (a : R[X]) → R[X][Y]) P.g) :
        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})))
      ((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}))) =
    1

Tactic:
rw [← map_mul, ← map_one (Ideal.Quotient.mk _), ← sub_eq_zero, ← map_sub, mul_comm]

Premises used: map_sub, sub_eq_zero, Ideal.Quotient.mk, map_mul, map_one, mul_comm