-- Lean 4 proof step from Mathlib.RingTheory.Smooth.NoetherianDescent (goal)
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
i : D.rels
⊢ Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i ∈
    (↑(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)))
have refine_1 : Membership.mem (α := MvPolynomial D.vars ↥(subalgebra R D)) (γ := Ideal (MvPolynomial D.vars ↥(subalgebra R D)))
  (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)
    (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))
      (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) (↥(subalgebra R D)) i) :
    MvPolynomial D.vars ↥(subalgebra R D))
Tactic: simp only [← AlgHom.comap_ker, Ideal.coe_comap, Set.mem_preimage, SetLike.mem_coe]