-- 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
refine_1 :
  ∀ (y : D.rels),
    Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) y ∈
      (↑(RingHom.ker (F :=
            MvPolynomial D.vars ↥(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
              (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))) :
        Set (MvPolynomial D.vars ↥(subalgebra R D)))
⊢ ∀ (a : MvPolynomial D.vars ↥(subalgebra R D)),
    Membership.mem (γ := 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))))
        a →
      Eq (α :=
        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
                (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) :
              (a : MvPolynomial D.vars ↥(subalgebra R D)) →
                MvPolynomial D.vars ↥(subalgebra R D) ⧸
                  RingHom.ker
                      (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                    2)
            a :
          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)
        (0 :
          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)

Tactic:
simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le, Set.range_subset_iff]

Premises used: Ideal.span_le, RingHom.mem_ker, SetLike.le_def, Set.range_subset_iff