awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels D.P.Ring)
      t =
    D.q i
⊢ ∃ (p' : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p'.IsHomogeneous 1 ∧
      (eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
            (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.vars ↥(subalgebra R D))
          p' =
        p i - X i
have refine_2 : IsHomogeneous.{0, u} (σ := D.rels) (R := MvPolynomial D.vars A)
  ((MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
    t)
  1
Tactic: refine ⟨t, .of_map hinj ?_, hinj ?_⟩
-- 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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels D.P.Ring)
      t =
    D.q i
refine_2 :
  IsHomogeneous.{0, u} (σ := D.rels) (R := MvPolynomial D.vars A)
    ((MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
      t)
    1
⊢ ∃ (p' : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))),
    p'.IsHomogeneous 1 ∧
      (eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
            (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.vars ↥(subalgebra R D))
          p' =
        p i - X i
have refine_2₁ : Eq (α := MvPolynomial D.vars A)
  ((MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
        (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
      ((eval (Presentation.relationOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (P := D.P) ↥(subalgebra R D)) :
          (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.vars ↥(subalgebra R D))
        t) :
    MvPolynomial D.vars A)
  ((MvPolynomial.map (algebraMap (↥(subalgebra R D)) A) :
        (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
      (p i - X i) :
    MvPolynomial D.vars A)
Tactic: refine ⟨t, .of_map hinj ?_, hinj ?_⟩
-- 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
hf₀ :
  Function.Surjective.{u + 1, u + 1} (α := MvPolynomial D.vars ↥(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))))) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) →
        MvPolynomial D.vars ↥(subalgebra R D) ⧸
          Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
i : D.vars
hinj :
  Function.Injective (α := MvPolynomial D.vars ↥(subalgebra R D)) (β := MvPolynomial D.vars A)
    (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
      (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A)
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht :
  (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels D.P.Ring)
      t =
    D.q i
⊢ IsHomogeneous.{0, u} (σ := D.rels) (R := MvPolynomial D.vars A)
    ((MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))) → MvPolynomial D.rels (MvPolynomial D.vars A))
      t)
    1
have refine_2 : (D.q i).IsHomogeneous 1
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.NoetherianDescent (hypothesis)
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
⊢ ∃ (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 hkerf : Eq (α := Ideal P.Ring) (RingHom.ker f) (Ideal.span (Set.range P.relation))
Tactic: have hkerf : RingHom.ker f = Ideal.span (.range P.relation) :=
    P.span_range_relation_eq_ker.symm
-- 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))
⊢ ∃ (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 obtain : ∀
  (σ :
    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),
  ∃ (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: obtain ⟨(σ : B →ₐ[A] MvPolynomial _ A ⧸ RingHom.ker f ^ 2), hsig⟩ :=
    (FormallySmooth.iff_split_surjection f P.algebraMap_surjective).mp inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.NoetherianDescent (hypothesis)
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
⊢ ∃ (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 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)
Tactic: have (i : _) := Ideal.Quotient.mk_surjective (σ <| P.val i)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.NoetherianDescent (hypothesis)
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)
⊢ ∃ (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 hdiag : AlgHom.comp (Ideal.Quotient.mkₐ A (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)) (aeval h) =
  σ.comp (aeval P.val)
Tactic: have hdiag : (Ideal.Quotient.mkₐ _ _).comp (aeval h) = σ.comp (aeval P.val) :=
    algHom_ext (by simp [hh])
-- 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
⊢ ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    FiniteType.{u_1, u} R ↥A₀ ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
have obtain : ∀ (A₀ : Subalgebra R A) (B₀ : Type u) (w : CommRing B₀) (w_1 : Algebra (↥A₀) B₀) (h0 : A₀.FG) (h1 : Smooth (↥A₀) B₀)
  (h2 : Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)),
  ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    FiniteType.{u_1, u} R ↥A₀ ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
Tactic: obtain ⟨A₀, B₀, _, _, h0, h1, h2⟩ := exists_subalgebra_fg R A B
-- 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
⊢ ∃ (A₀ : Type u) (B₀ : Type u) (x : CommRing A₀) (x_1 : CommRing B₀) (x_2 : Algebra R A₀) (x_3 : Algebra A₀ A) (x_4 :
    Algebra A₀ B₀),
    Function.Injective (α := A₀) (β := A) (⇑(algebraMap A₀ A) : (a : A₀) → A) ∧
      FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)
have obtain : ∀ (A₀ : Subalgebra R A) (B₀ : Type u) (w : CommRing B₀) (w_1 : Algebra (↥A₀) B₀) (hA₀ : A₀.FG),
  Smooth (↥A₀) B₀ →
    Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀) →
      ∃ (A₀ : Type u) (B₀ : Type u) (x : CommRing A₀) (x_1 : CommRing B₀) (x_2 : Algebra R A₀) (x_3 : Algebra A₀ A) (x_4
        : Algebra A₀ B₀),
        Function.Injective (α := A₀) (β := A) (⇑(algebraMap A₀ A) : (a : A₀) → A) ∧
          FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)
Tactic: obtain ⟨A₀, B₀, _, _, hA₀, _, _⟩ := exists_subalgebra_fg R A B
-- 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
A₀ : Subalgebra R A
B₀ : Type u
w_1 : CommRing B₀
w_2 : Algebra (↥A₀) B₀
hA₀ : A₀.FG
left : Smooth (↥A₀) B₀
right : Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
w w₁ : Type u
⊢ ∃ (A₀ : Type u) (B₀ : Type u) (x : CommRing A₀) (x_1 : CommRing B₀) (x_2 : Algebra R A₀) (x_3 : Algebra A₀ A) (x_4 :
    Algebra A₀ B₀),
    Function.Injective (α := A₀) (β := A) (⇑(algebraMap A₀ A) : (a : A₀) → A) ∧
      FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)
have w₂ : CommRing ↥A₀
Tactic: use A₀, B₀, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
    Subtype.val_injective, ⟨A₀.fg_top.mpr hA₀⟩, inferInstance
-- 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
A₀ : Subalgebra R A
B₀ : Type u
w_1 : CommRing B₀
w_2 : Algebra (↥A₀) B₀
hA₀ : A₀.FG
left : Smooth (↥A₀) B₀
right : Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
w w₁ : Type u
w₂ : CommRing ↥A₀
w₃ : CommRing B₀
⊢ ∃ (A₀ : Type u) (B₀ : Type u) (x : CommRing A₀) (x_1 : CommRing B₀) (x_2 : Algebra R A₀) (x_3 : Algebra A₀ A) (x_4 :
    Algebra A₀ B₀),
    Function.Injective (α := A₀) (β := A) (⇑(algebraMap A₀ A) : (a : A₀) → A) ∧
      FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)
have w₄ : Algebra.{u_1, u} R ↥A₀
Tactic: use A₀, B₀, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
    Subtype.val_injective, ⟨A₀.fg_top.mpr hA₀⟩, inferInstance
-- 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
A₀ : Subalgebra R A
B₀ : Type u
w_1 : CommRing B₀
w_2 : Algebra (↥A₀) B₀
hA₀ : A₀.FG
left : Smooth (↥A₀) B₀
right : Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
w w₁ : Type u
w₂ : CommRing ↥A₀
w₃ : CommRing B₀
w₄ : Algebra.{u_1, u} R ↥A₀
⊢ ∃ (A₀ : Type u) (B₀ : Type u) (x : CommRing A₀) (x_1 : CommRing B₀) (x_2 : Algebra R A₀) (x_3 : Algebra A₀ A) (x_4 :
    Algebra A₀ B₀),
    Function.Injective (α := A₀) (β := A) (⇑(algebraMap A₀ A) : (a : A₀) → A) ∧
      FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)
have w₅ : Algebra (↥A₀) A
Tactic: use A₀, B₀, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
    Subtype.val_injective, ⟨A₀.fg_top.mpr hA₀⟩, inferInstance
-- 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
A₀ : Subalgebra R A
B₀ : Type u
w_1 : CommRing B₀
w_2 : Algebra (↥A₀) B₀
hA₀ : A₀.FG
left : Smooth (↥A₀) B₀
right : Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
w w₁ : Type u
w₂ : CommRing ↥A₀
w₃ : CommRing B₀
w₄ : Algebra.{u_1, u} R ↥A₀
w₅ : Algebra (↥A₀) A
w₆ : Algebra (↥A₀) B₀
⊢ ∃ (A₀ : Type u) (B₀ : Type u) (x : CommRing A₀) (x_1 : CommRing B₀) (x_2 : Algebra R A₀) (x_3 : Algebra A₀ A) (x_4 :
    Algebra A₀ B₀),
    Function.Injective (α := A₀) (β := A) (⇑(algebraMap A₀ A) : (a : A₀) → A) ∧
      FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)
have left : Function.Injective (α := ↥A₀) (β := A) (⇑(algebraMap (↥A₀) A) : (a : ↥A₀) → A)
Tactic: use A₀, B₀, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
    Subtype.val_injective, ⟨A₀.fg_top.mpr hA₀⟩, inferInstance
-- 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
A₀ : Subalgebra R A
B₀ : Type u
w_1 : CommRing B₀
w_2 : Algebra (↥A₀) B₀
hA₀ : A₀.FG
left_1 : Smooth (↥A₀) B₀
right : Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
w w₁ : Type u
w₂ : CommRing ↥A₀
w₃ : CommRing B₀
w₄ : Algebra.{u_1, u} R ↥A₀
w₅ : Algebra (↥A₀) A
w₆ : Algebra (↥A₀) B₀
left : Function.Injective (α := ↥A₀) (β := A) (⇑(algebraMap (↥A₀) A) : (a : ↥A₀) → A)
⊢ ∃ (A₀ : Type u) (B₀ : Type u) (x : CommRing A₀) (x_1 : CommRing B₀) (x_2 : Algebra R A₀) (x_3 : Algebra A₀ A) (x_4 :
    Algebra A₀ B₀),
    Function.Injective (α := A₀) (β := A) (⇑(algebraMap A₀ A) : (a : A₀) → A) ∧
      FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)
have left₁ : FiniteType.{u_1, u} R ↥A₀
Tactic: use A₀, B₀, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance,
    Subtype.val_injective, ⟨A₀.fg_top.mpr hA₀⟩, inferInstance
-- 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
n : ℕ
inst_5 : IsStandardSmoothOfRelativeDimension n A B
⊢ ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    A₀.FG ∧ IsStandardSmoothOfRelativeDimension n (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
have obtain : ∀ (ι σ : Type) (w : Finite σ),
  Finite ι →
    ∀ (P : SubmersivePresentation A B ι σ) (hP : P.dimension = n),
      ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
        A₀.FG ∧ IsStandardSmoothOfRelativeDimension n (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
Tactic: obtain ⟨ι, σ, _, _, P, hP⟩ := IsStandardSmoothOfRelativeDimension.out (n := n) (R := A) (S := B)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.NoetherianDescent (hypothesis)
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
n : ℕ
inst_5 : IsStandardSmoothOfRelativeDimension n A B
ι σ : Type
w : Finite σ
w_1 : Finite ι
P : SubmersivePresentation A B ι σ
hP : P.dimension = n
A₀ : Subalgebra R A := adjoin R P.coeffs
⊢ ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    A₀.FG ∧ IsStandardSmoothOfRelativeDimension n (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
have this : P.HasCoeffs ↥A₀
Tactic: have : P.HasCoeffs A₀ := ⟨by simp [A₀]⟩
-- 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 : Etale A B
⊢ ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    A₀.FG ∧ Etale (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
have simp : IsStandardSmoothOfRelativeDimension 0 A B →
  ∃ (A₀ : Subalgebra R A) (B₀ : Type u) (x : CommRing B₀) (x_1 : Algebra (↥A₀) B₀),
    A₀.FG ∧ IsStandardSmoothOfRelativeDimension 0 (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)
Tactic: simp only [Etale.iff_isStandardSmoothOfRelativeDimension_zero] at *
Cleared hypotheses: inst_5
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (goal)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
⊢ FormallySmooth.{u_1, u_3} R (A i)
have g : A i →ₐ[R]
  ((i : I) → A i) ⧸
    HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
      (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2
Tactic: fapply FormallySmooth.of_split (Pi.evalAlgHom R A i)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Pi (goal)
Goal:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst : CommRing R
inst_1 : (i : I) → CommRing (A i)
inst_2 : (i : I) → Algebra.{u_1, u_3} R (A i)
inst_3 : FormallySmooth R ((i : I) → A i)
i : I
g :
  A i →ₐ[R]
    ((i : I) → A i) ⧸
      HPow.hPow (α := Ideal ((i : I) → A i)) (β := ℕ)
        (RingHom.ker (F := ((i : I) → A i) →+* A i) (AlgHom.toRingHom (Pi.evalAlgHom R A i))) 2
⊢ FormallySmooth.{u_1, u_3} R (A i)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: fapply FormallySmooth.of_split (Pi.evalAlgHom R A i)