-- 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
inst_5 : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : Eq (α := Ideal P.Ring) (RingHom.ker f) (Ideal.span (Set.range P.relation))
σ :
  B →ₐ[A]
    MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2
hsig : f.kerSquareLift.comp σ = AlgHom.id A B
h :
  (i : Fin (Presentation.ofFinitePresentationVars A B)) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)),
    Eq (α :=
      MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸
        HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)
      ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2) :
            (a : MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A) →
              MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2)
          (h i) :
        MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸
          HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)
      ((σ : (a : B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2) (P.val i) :
        MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸
          HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)
hdiag :
  AlgHom.comp (Ideal.Quotient.mkₐ A (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)) (aeval h) =
    σ.comp (aeval P.val)
this :
  ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)),
    Eq (α :=
      MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸
        HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)
      ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2) :
            (a : MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A) →
              MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2)
          ((aeval h :
              (a : MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A) →
                MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
            (P.relation j)) :
        MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸
          HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)
      (0 :
        MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸
          HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)
⊢ ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)),
    ∃ (p :
      MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
        (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)),
      p.IsHomogeneous 2 ∧
        Eq (α := MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
          ((eval P.relation :
                (a :
                    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
                      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)) →
                  MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
              p :
            MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
          ((aeval h :
                (a : MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A) →
                  MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
              (P.relation j) :
            MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)

Tactic:
simp_rw [Ideal.Quotient.eq_zero_iff_mem, hkerf,
    Ideal.mem_span_pow_iff_exists_isHomogeneous] at this

Premises used: Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_pow_iff_exists_isHomogeneous