-- 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_1 : StandardEtalePair R
P : StandardEtalePresentation R S
rw :
  Eq (α :=
    Ideal
      (Algebra.Generators.ofAlgHom
          ((P.lift P.x ⋯).comp
            ((↑P.equivMvPolynomialQuotient.symm :
                  MvPolynomial (Fin 2) R ⧸
                      Ideal.span
                        {(Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                            ((C : (a : R[X]) → R[X][Y]) P.f),
                          (Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                            (Y * (C : (a : R[X]) → R[X][Y]) P.g - 1)} →ₐ[R]
                    P.Ring).comp
              (Ideal.Quotient.mkₐ R
                (Ideal.span
                  (insert (α := MvPolynomial (Fin 2) R)
                    ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                        ((C : (a : R[X]) → R[X][Y]) P.f) :
                      MvPolynomial (Fin 2) R)
                    (singleton (α := MvPolynomial (Fin 2) R)
                      ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1) :
                        MvPolynomial (Fin 2) R)))))))
          ⋯).Ring)
    (Ideal.span
        (Set.range (ι := Fin 2)
          ![(Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) ((C : (a : R[X]) → R[X][Y]) P.f),
            (Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
              (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1)]) :
      Ideal
        (Algebra.Generators.ofAlgHom
            ((P.lift P.x ⋯).comp
              ((↑P.equivMvPolynomialQuotient.symm :
                    MvPolynomial (Fin 2) R ⧸
                        Ideal.span
                          {(Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                              ((C : (a : R[X]) → R[X][Y]) P.f),
                            (Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                              (Y * (C : (a : R[X]) → R[X][Y]) P.g - 1)} →ₐ[R]
                      P.Ring).comp
                (Ideal.Quotient.mkₐ R
                  (Ideal.span
                    (insert (α := MvPolynomial (Fin 2) R)
                      ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                          ((C : (a : R[X]) → R[X][Y]) P.f) :
                        MvPolynomial (Fin 2) R)
                      (singleton (α := MvPolynomial (Fin 2) R)
                        ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1) :
                          MvPolynomial (Fin 2) R)))))))
            ⋯).Ring)
    (RingHom.ker (F :=
        MvPolynomial (Fin 2) R →+*
          HasQuotient.Quotient (MvPolynomial (Fin 2) R) (B := Ideal (MvPolynomial (Fin 2) R))
            (Ideal.span
              (insert (α := MvPolynomial (Fin 2) R)
                ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                    ((C : (a : R[X]) → R[X][Y]) P.f) :
                  MvPolynomial (Fin 2) R)
                (singleton (α := MvPolynomial (Fin 2) R)
                  ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                      (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1) :
                    MvPolynomial (Fin 2) R)))))
        (↑(Ideal.Quotient.mkₐ R
              (Ideal.span
                (insert (α := MvPolynomial (Fin 2) R)
                  ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                      ((C : (a : R[X]) → R[X][Y]) P.f) :
                    MvPolynomial (Fin 2) R)
                  (singleton (α := MvPolynomial (Fin 2) R)
                    ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1) :
                      MvPolynomial (Fin 2) R))))) :
          MvPolynomial (Fin 2) R →+*
            MvPolynomial (Fin 2) R ⧸
              Ideal.span
                {(Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                    ((C : (a : R[X]) → R[X][Y]) P.f),
                  (Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                    (Y * (C : (a : R[X]) → R[X][Y]) P.g - 1)}) :
      Ideal (MvPolynomial (Fin 2) R))
⊢ Ideal.span
      (Set.range (ι := Fin 2)
        ![(Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R) ((C : (a : R[X]) → R[X][Y]) P.f),
          (Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
            (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1)]) =
    (Algebra.Generators.ofAlgHom
        ((P.lift P.x ⋯).comp
          ((↑P.equivMvPolynomialQuotient.symm :
                MvPolynomial (Fin 2) R ⧸
                    Ideal.span
                      {(Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                          ((C : (a : R[X]) → R[X][Y]) P.f),
                        (Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                          (Y * (C : (a : R[X]) → R[X][Y]) P.g - 1)} →ₐ[R]
                  P.Ring).comp
            (Ideal.Quotient.mkₐ R
              (Ideal.span
                (insert (α := MvPolynomial (Fin 2) R)
                  ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                      ((C : (a : R[X]) → R[X][Y]) P.f) :
                    MvPolynomial (Fin 2) R)
                  (singleton (α := MvPolynomial (Fin 2) R)
                    ((Bivariate.equivMvPolynomial R : (a : R[X][Y]) → MvPolynomial (Fin 2) R)
                        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) P.g : R[X][Y]) - 1) :
                      MvPolynomial (Fin 2) R)))))))
        ⋯).ker

Tactic:
rw [Algebra.Generators.ker_ofAlgHom, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom,
      AlgHom.comp_toRingHom,
      RingHom.ker_comp_of_injective _ (by exact P.lift_bijective.injective),
      RingHom.ker_comp_of_injective _ (by exact P.equivMvPolynomialQuotient.symm.injective)]

Premises used: AlgHom.comp_toRingHom, RingHom.ker_comp_of_injective, AlgHom.toRingHom_eq_coe, Algebra.Generators.ker_ofAlgHom