-- 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
choose :
  ∀ (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),
    ∃ (σ₀ :
      Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
          ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
        MvPolynomial D.vars ↥(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),
      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))))))
          σ₀ =
        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))
⊢ ∃ (σ₀ :
    Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
        ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
      MvPolynomial D.vars ↥(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),
    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))))))
        σ₀ =
      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))

Tactic:
choose p hp using fun i ↦ (D.h i).mem_range_map_iff_coeffs_subset.mpr (D.coeffs_h_subset R i)

Premises used: Iff.mpr, MvPolynomial.mem_range_map_iff_coeffs_subset, _private.0.Algebra.Smooth.DescentAux.hp, _private.0.Algebra.Smooth.DescentAux.p, _private.0.Algebra.Smooth.DescentAux.coeffs_h_subset