-- 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
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
this :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)),
    ∃ (a : MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A),
      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)
            a :
          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)
⊢ ∃ (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₀)
have choose : ∀
  (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)),
  ∃ (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: choose h hh using this
Cleared hypotheses: this