-- 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_1 : 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)
p :
  (j : Fin (Presentation.ofFinitePresentationRels A B)) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp :
  ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)),
    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 j) :
        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)
hsig : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (f : (a : P.Ring) → B) (h i) = P.val i
q :
  (i : Fin (Presentation.ofFinitePresentationVars A B)) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B)) P.Ring
hqhom : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (q i).IsHomogeneous 1
hq :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)),
    (eval P.relation : (a : MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B)) P.Ring) → P.Ring) (q i) =
      h i - X i
D : DescentAux A B :=
  { vars := Fin (Presentation.ofFinitePresentationVars A B), rels := Fin (Presentation.ofFinitePresentationRels A B),
    P := P, σ := σ, h := h, p := p, hphom := homog, hp := hp, q := q, hqhom := hqhom, hq := hq }
this : P.HasCoeffs ↥(DescentAux.subalgebra R D)
σ₀ :
  Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
      ↥(DescentAux.subalgebra R D) →ₐ[↥(DescentAux.subalgebra R D)]
    MvPolynomial D.vars ↥(DescentAux.subalgebra R D) ⧸
      HPow.hPow (α := Ideal (MvPolynomial D.vars ↥(DescentAux.subalgebra R D))) (β := ℕ)
        (RingHom.ker (F :=
          MvPolynomial D.vars ↥(DescentAux.subalgebra R D) →ₐ[↥(DescentAux.subalgebra R D)]
            HasQuotient.Quotient (MvPolynomial D.vars ↥(DescentAux.subalgebra R D)) (B :=
              Ideal (MvPolynomial D.vars ↥(DescentAux.subalgebra R D)))
              (Ideal.span
                (Set.range (ι := D.rels)
                  (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                    ↥(DescentAux.subalgebra R D)))))
          (Ideal.Quotient.mkₐ (↥(DescentAux.subalgebra R D))
            (Ideal.span
              (Set.range (ι := D.rels)
                (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                  ↥(DescentAux.subalgebra R D))))))
        2
hσ₀ :
  AlgHom.comp
      (AlgHom.kerSquareLift
        (Ideal.Quotient.mkₐ (↥(DescentAux.subalgebra R D))
          (Ideal.span
            (Set.range (ι := D.rels)
              (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P)
                ↥(DescentAux.subalgebra R D))))))
      σ₀ =
    AlgHom.id (↥(DescentAux.subalgebra R D))
      (Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
        ↥(DescentAux.subalgebra R D))
⊢ ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
⟨D.subalgebra R, P.ModelOfHasCoeffs (D.subalgebra R), inferInstance, inferInstance,
    D.fg_subalgebra R, ⟨.of_split _ σ₀ hσ₀, inferInstance⟩,
    ⟨(P.tensorModelOfHasCoeffsEquiv (D.subalgebra R)).symm⟩⟩

Premises used: AlgEquiv.symm, Algebra.Smooth.mk, Algebra.Presentation.ModelOfHasCoeffs, Membership.mem, inferInstance, Subtype, Nonempty.intro, Algebra.Presentation.tensorModelOfHasCoeffsEquiv, _private.0.Algebra.Smooth.DescentAux.fg_subalgebra, And.intro, Exists.intro, Algebra.FormallySmooth.of_split, _private.0.Algebra.Smooth.DescentAux.subalgebra