-- Lean 4 proof step from Mathlib.RingTheory.Etale.StandardEtale (goal)
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
⊢ 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
have rw : Eq (α :=
  Ideal
    (Algebra.Generators.ofAlgHom
        ((P.lift P.x sorry).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)))))))
        sorry).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 sorry).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)))))))
          sorry).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))
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)]