-- Module: Mathlib.RingTheory.Smooth.NoetherianDescent
Goal:
R : Type u_1
inst : CommRing R
A : Type u
B : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra A B
D : DescentAux A B
p : (i : D.vars) → MvPolynomial D.vars ↥(subalgebra R D)
hp :
  ∀ (i : D.vars),
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
        (p i) =
      D.h i
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(subalgebra R D)) (β :=
    HasQuotient.Quotient (MvPolynomial D.vars ↥(subalgebra R D)) (B := Ideal (MvPolynomial D.vars ↥(subalgebra R D)))
      (Ideal.span
        (Set.range (ι := D.rels)
          (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)))))
    (⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
          (Ideal.span
            (Set.range (ι := D.rels)
              (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
refine_2 :
  ∃ (p' : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p'.IsHomogeneous 1 ∧
      (eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
            (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.vars ↥(subalgebra R D))
          p' =
        p i - X i
⊢ Eq (α :=
    HasQuotient.Quotient (MvPolynomial D.vars ↥(subalgebra R D)) (B := Ideal (MvPolynomial D.vars ↥(subalgebra R D)))
      (Ideal.span
        (Set.range (ι := D.rels)
          (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)))))
    ((AlgHom.comp (B :=
            HasQuotient.Quotient (MvPolynomial D.vars ↥(subalgebra R D)) (B :=
              Ideal (MvPolynomial D.vars ↥(subalgebra R D)))
              (Ideal.span
                (Set.range (ι := D.rels)
                  (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)))))
            (AlgHom.comp
              (AlgHom.kerSquareLift
                (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                  (Ideal.span
                    (Set.range (ι := D.rels)
                      (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                        ↥(subalgebra R D))))))
              (Ideal.Quotient.liftₐ
                (Ideal.span
                  (Set.range (ι := D.rels)
                    (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                      ↥(subalgebra R D))))
                (AlgHom.comp
                  (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                    (HPow.hPow (α := Ideal (MvPolynomial D.vars ↥(subalgebra R D))) (β := ℕ)
                      (RingHom.ker (F :=
                        MvPolynomial D.vars ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
                          HasQuotient.Quotient (MvPolynomial D.vars ↥(subalgebra R D)) (B :=
                            Ideal (MvPolynomial D.vars ↥(subalgebra R D)))
                            (Ideal.span
                              (Set.range (ι := D.rels)
                                (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                                  ↥(subalgebra R D)))))
                        (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                          (Ideal.span
                            (Set.range (ι := D.rels)
                              (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                                ↥(subalgebra R D))))))
                      2))
                  (aeval p))
                ⋯))
            (Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (Ideal.span
                (Set.range (ι := D.rels)
                  (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                    ↥(subalgebra R D))))) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) →
            MvPolynomial D.vars ↥(subalgebra R D) ⧸
              Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
        (X i) :
      HasQuotient.Quotient (MvPolynomial D.vars ↥(subalgebra R D)) (B := Ideal (MvPolynomial D.vars ↥(subalgebra R D)))
        (Ideal.span
          (Set.range (ι := D.rels)
            (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)))))
    ((AlgHom.comp
            (AlgHom.id (↥(subalgebra R D))
              (Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
                ↥(subalgebra R D)))
            (Ideal.Quotient.mkₐ (↥(subalgebra R D))
              (Ideal.span
                (Set.range (ι := D.rels)
                  (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                    ↥(subalgebra R D))))) :
          (a : MvPolynomial D.vars ↥(subalgebra R D)) →
            MvPolynomial D.vars ↥(subalgebra R D) ⧸
              Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
        (X i) :
      HasQuotient.Quotient (MvPolynomial D.vars ↥(subalgebra R D)) (B := Ideal (MvPolynomial D.vars ↥(subalgebra R D)))
        (Ideal.span
          (Set.range (ι := D.rels)
            (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)))))

Tactic:
suffices h : ∃ p', p'.IsHomogeneous 1 ∧ (eval (D.P.relationOfHasCoeffs (D.subalgebra R))) p' =
        p i - X i by
      -- Reducible def-eq issues caused by `RingHom.ker f.toRingHom` discrepancies
      -- Can be fixed after #25138.
      apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr
      simpa [Ideal.mem_span_iff_exists_isHomogeneous, hp]