awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : (↑(basicOpen f) : Set (PrimeSpectrum A)) ⊆ Module.freeLocus A Ω[A⁄R]
⊢ Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])

Tactic:
rw [Module.basicOpen_subset_freeLocus_iff] at hf

Premises used: Module.basicOpen_subset_freeLocus_iff
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
⊢ FinitePresentation A (Localization.Away f)

Tactic:
have : Algebra.FinitePresentation A (Localization.Away f) :=
    IsLocalization.Away.finitePresentation f
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this : FinitePresentation A (Localization.Away f)
⊢ FinitePresentation.{u_1, u_2} R (Localization.Away f)

Tactic:
have : Algebra.FinitePresentation R (Localization.Away f) :=
    .trans _ A _
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this : FinitePresentation.{u_1, u_2} R (Localization.Away f)
have :
  ∀ (this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]),
    IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)
⊢ IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)

Tactic:
have := IsLocalizedModule.iso (.powers f)
      (KaehlerDifferential.map R R A (Localization.Away f))
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
have :
  ∀ (this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]),
    IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)
⊢ IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)

Tactic:
have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this_3 : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]
⊢ Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R]

Tactic:
have := Module.Projective.of_equiv this
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this_3 : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
this_4 : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]
this : Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R]
rw :
  IsOpen (X := PrimeSpectrum Af)
    ((zeroLocus (↑(Module.annihilator Af (H1Cotangent R Af)) : Set Af))ᶜ ∩ Module.freeLocus Af Ω[Af⁄R])
⊢ IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)

Tactic:
rw [smoothLocus_eq_compl_support_inter, Module.support_eq_zeroLocus]

Premises used: Module.support_eq_zeroLocus, Algebra.smoothLocus_eq_compl_support_inter
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this_3 : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
this_4 : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]
this : Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R]
⊢ IsOpen (X := PrimeSpectrum Af)
    ((zeroLocus (↑(Module.annihilator Af (H1Cotangent R Af)) : Set Af))ᶜ ∩ Module.freeLocus Af Ω[Af⁄R])

Tactic:
(isClosed_zeroLocus _).isOpen_compl.inter Module.isOpen_freeLocus

Premises used: IsClosed.isOpen_compl, Module.isOpen_freeLocus, IsOpen.inter
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this_3 : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]
this_4 : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]
this : Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R]
⊢ IsOpen (X := PrimeSpectrum Af)
    ((zeroLocus (↑(Module.annihilator Af (H1Cotangent R Af)) : Set Af))ᶜ ∩ Module.freeLocus Af Ω[Af⁄R])

Tactic:
exact (isClosed_zeroLocus _).isOpen_compl.inter Module.isOpen_freeLocus

Premises used: IsClosed.isOpen_compl, Module.isOpen_freeLocus, IsOpen.inter
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this : FinitePresentation.{u_1, u_2} R (Localization.Away f)
⊢ IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)

Tactic:
have : IsOpen (smoothLocus R Af) := by
    have := IsLocalizedModule.iso (.powers f)
      (KaehlerDifferential.map R R A (Localization.Away f))
    have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
    have := Module.Projective.of_equiv this
    rw [smoothLocus_eq_compl_support_inter, Module.support_eq_zeroLocus]
    exact (isClosed_zeroLocus _).isOpen_compl.inter Module.isOpen_freeLocus
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this : IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)
⊢ IsOpen (Set.preimage (β := PrimeSpectrum A) (comap (algebraMap A Af)) (smoothLocus R A))

Tactic:
rw [← smoothLocus_comap_of_isLocalization f] at this

Premises used: Algebra.smoothLocus_comap_of_isLocalization
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this : IsOpen (Set.preimage (β := PrimeSpectrum A) (comap (algebraMap A Af)) (smoothLocus R A))
⊢ IsOpen (X := PrimeSpectrum A)
    (comap (algebraMap A Af) '' Set.preimage (β := PrimeSpectrum A) (comap (algebraMap A Af)) (smoothLocus R A))

Tactic:
replace this := (PrimeSpectrum.localization_away_isOpenEmbedding Af f).isOpenMap _ this
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this :
  IsOpen (X := PrimeSpectrum A)
    (comap (algebraMap A Af) '' Set.preimage (β := PrimeSpectrum A) (comap (algebraMap A Af)) (smoothLocus R A))
⊢ IsOpen (smoothLocus R A ∩ (↑(basicOpen f) : Set (PrimeSpectrum A)))

Tactic:
rw [Set.image_preimage_eq_inter_range, localization_away_comap_range Af f] at this

Premises used: Set.image_preimage_eq_inter_range, PrimeSpectrum.localization_away_comap_range
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this : IsOpen (smoothLocus R A ∩ (↑(basicOpen f) : Set (PrimeSpectrum A)))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
⟨_, Set.inter_subset_left, this, hx, hxf⟩

Premises used: Set.inter_subset_left, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) x
f : A
hxf : x ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this_1 : FinitePresentation A (Localization.Away f)
this_2 : FinitePresentation.{u_1, u_2} R (Localization.Away f)
this : IsOpen (smoothLocus R A ∩ (↑(basicOpen f) : Set (PrimeSpectrum A)))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
exact ⟨_, Set.inter_subset_left, this, hx, hxf⟩
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
obtain :
  ∀ (f : A) (hxf : { asIdeal := p, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(basicOpen f) : Set (PrimeSpectrum A)))
    (hf : (↑(basicOpen f) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A),
    ∃ f ∉ p, Smooth.{u_2, u_1} R (Localization.Away f)
⊢ ∃ f ∉ p, Smooth.{u_2, u_1} R (Localization.Away f)

Tactic:
obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hxf, hf⟩ :=
    isBasis_basic_opens.exists_subset_of_mem_open ‹⟨p, ‹_›⟩ ∈ smoothLocus R A› isOpen_smoothLocus

Premises used: Algebra.isOpen_smoothLocus, PrimeSpectrum.isBasis_basic_opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
f : A
hxf : { asIdeal := p, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : (↑(basicOpen f) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A
⊢ f ∉ p

Tactic:
simpa using hxf
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
f : A
hxf : { asIdeal := p, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : (↑(basicOpen f) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A
refine : FormallySmooth.{u_1, u_2} R (Localization.Away f)
⊢ ∃ f ∉ p, Smooth.{u_2, u_1} R (Localization.Away f)

Tactic:
refine ⟨f, by simpa using hxf, ⟨?_, inferInstance⟩⟩
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
p : Ideal A
inst_4 : p.IsPrime
inst_5 : IsSmoothAt R p
f : A
hxf : { asIdeal := p, isPrime := inst_4 : PrimeSpectrum A } ∈ (↑(basicOpen f) : Set (PrimeSpectrum A))
hf : (↑(basicOpen f) : Set (PrimeSpectrum A)) ⊆ smoothLocus R A
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hf : FormallySmooth.{u_1, u_2} R (Localization.Away f)), FormallySmooth.{u_1, u_2} R (Localization.Away f)
⊢ FormallySmooth.{u_1, u_2} R (Localization.Away f)

Tactic:
rwa [basicOpen_subset_smoothLocus_iff] at hf

Premises used: Algebra.basicOpen_subset_smoothLocus_iff
-- 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
D : DescentAux A B
⊢ IsScalarTower (↥(subalgebra R D)) A B

Tactic:
inferInstanceAs <| IsScalarTower (Algebra.adjoin _ _) _ _

Premises used: _private.0.Algebra.Smooth.DescentAux.instIsScalarTowerSubtypeMemSubalgebraSubalgebra._proof_1
-- 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
D : DescentAux A B
⊢ FaithfulSMul (↥(subalgebra R D)) A

Tactic:
inferInstanceAs <| FaithfulSMul (Algebra.adjoin _ _) _

Premises used: _private.0.Algebra.Smooth.DescentAux.instFaithfulSMulSubtypeMemSubalgebraSubalgebra._proof_1
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
⊢ Subalgebra.FG (subalgebra R D)

Tactic:
Subalgebra.fg_def.mpr ⟨_, ?_, rfl⟩

Premises used: Iff.mpr, Subalgebra.fg_def, And.intro, Exists.intro, rfl
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
refine :
  (D.P.coeffs ∪
      (((⋃ (i : D.vars), (↑(D.h i).coeffs : Set A)) ∪ ⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A)) ∪
        ⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))).Finite
⊢ Subalgebra.FG (subalgebra R D)

Tactic:
refine Subalgebra.fg_def.mpr ⟨_, ?_, rfl⟩

Premises used: Iff.mpr, Subalgebra.fg_def, And.intro, Exists.intro, rfl
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
⊢ (D.P.coeffs ∪
      (((⋃ (i : D.vars), (↑(D.h i).coeffs : Set A)) ∪ ⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A)) ∪
        ⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))).Finite

Tactic:
.union ?_ (.union (.union ?_ ?_) ?_)

Premises used: Set.Finite.union
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
refine_1 : D.P.coeffs.Finite
refine_2 : Set.Finite.{u} (α := A) (⋃ (i : D.vars), (↑(D.h i).coeffs : Set A))
refine_3 : Set.Finite.{u} (α := A) (⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A))
refine_4 : Set.Finite.{u} (α := A) (⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))
⊢ (D.P.coeffs ∪
      (((⋃ (i : D.vars), (↑(D.h i).coeffs : Set A)) ∪ ⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A)) ∪
        ⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))).Finite

Tactic:
refine .union ?_ (.union (.union ?_ ?_) ?_)
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
⊢ D.P.coeffs.Finite

Tactic:
Presentation.finite_coeffs

Premises used: Algebra.Presentation.finite_coeffs
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
⊢ D.P.coeffs.Finite

Tactic:
exact Presentation.finite_coeffs

Premises used: Algebra.Presentation.finite_coeffs
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
⊢ Set.Finite.{u} (α := A) (⋃ (i : D.vars), (↑(D.h i).coeffs : Set A))

Tactic:
Set.finite_iUnion fun i ↦ Finset.finite_toSet _

Premises used: Set.finite_iUnion, MvPolynomial.coeffs, Finset.finite_toSet, _private.0.Algebra.Smooth.DescentAux.h
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
⊢ Set.Finite.{u} (α := A) (⋃ (i : D.vars), (↑(D.h i).coeffs : Set A))

Tactic:
refine Set.finite_iUnion fun i ↦ Finset.finite_toSet _

Premises used: Set.finite_iUnion, Finset.finite_toSet
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
⊢ Set.Finite.{u} (α := A) (⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A))

Tactic:
Set.finite_iUnion fun i ↦ ?_

Premises used: Set.finite_iUnion
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
refine_3 : ∀ (i : D.vars), Set.Finite.{u} (α := A) (⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A))
⊢ Set.Finite.{u} (α := A) (⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A))

Tactic:
refine Set.finite_iUnion fun i ↦ ?_

Premises used: Set.finite_iUnion
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
i : D.vars
⊢ Set.Finite.{u} (α := A) (⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A))

Tactic:
Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)

Premises used: MvPolynomial.coeffs, Finset.finite_toSet, Set.Finite.biUnion
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
i : D.vars
⊢ Set.Finite.{u} (α := A) (⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A))

Tactic:
exact Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)

Premises used: Finset.finite_toSet, Set.Finite.biUnion
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
⊢ Set.Finite.{u} (α := A) (⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))

Tactic:
Set.finite_iUnion fun i ↦ ?_

Premises used: Set.finite_iUnion
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
refine_4 : ∀ (i : D.rels), Set.Finite.{u} (α := A) (⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))
⊢ Set.Finite.{u} (α := A) (⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))

Tactic:
refine Set.finite_iUnion fun i ↦ ?_

Premises used: Set.finite_iUnion
-- 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
D : DescentAux A B
inst_5 : Finite D.vars
inst_6 : Finite D.rels
i : D.rels
⊢ Set.Finite.{u} (α := A) (⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))

Tactic:
Set.Finite.biUnion (Finset.finite_toSet _) (fun i hi ↦ Finset.finite_toSet _)

Premises used: MvPolynomial.coeffs, Finset.finite_toSet, Set.Finite.biUnion