awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
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]
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
have hf₁ : Module.Projective.{u_2, u_2} (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Tactic: rw [Module.basicOpen_subset_freeLocus_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
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
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
have this : FinitePresentation A (Localization.Away f)
Tactic: have : Algebra.FinitePresentation A (Localization.Away f) :=
    IsLocalization.Away.finitePresentation f
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
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)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
have this₁ : FinitePresentation.{u_1, u_2} R (Localization.Away f)
Tactic: have : Algebra.FinitePresentation R (Localization.Away f) :=
    .trans _ A _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
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)
have have : ∀ (this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[A] Ω[Localization.Away f⁄R]),
  IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)
Tactic: have := IsLocalizedModule.iso (.powers f)
      (KaehlerDifferential.map R R A (Localization.Away f))
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
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]
⊢ IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)
have have : ∀ (this : LocalizedModule (Submonoid.powers f) Ω[A⁄R] ≃ₗ[Localization.Away f] Ω[Localization.Away f⁄R]),
  IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)
Tactic: have := this.extendScalarsOfIsLocalization (.powers f) (Localization.Away f)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
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]
⊢ IsOpen (X := PrimeSpectrum Af) (smoothLocus R Af)
have this₁ : Module.Projective.{u_2, u_2} (Localization.Away f) Ω[Localization.Away f⁄R]
Tactic: have := Module.Projective.of_equiv this
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
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) (smoothLocus R Af)
have rw : IsOpen (X := PrimeSpectrum Af)
  ((zeroLocus (↑(Module.annihilator Af (H1Cotangent R Af)) : Set Af))ᶜ ∩ Module.freeLocus Af Ω[Af⁄R])
Tactic: rw [smoothLocus_eq_compl_support_inter, Module.support_eq_zeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
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)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
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)
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
have this₁ : IsOpen (Set.preimage (β := PrimeSpectrum A) (comap (algebraMap A Af)) (smoothLocus R A))
Tactic: rw [← smoothLocus_comap_of_isLocalization f] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
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))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (hypothesis)
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))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
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 ∉ p, Smooth.{u_2, u_1} R (Localization.Away f)
have 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)
Tactic: obtain ⟨_, ⟨_, ⟨f, rfl⟩, rfl⟩, hxf, hf⟩ :=
    isBasis_basic_opens.exists_subset_of_mem_open ‹⟨p, ‹_›⟩ ∈ smoothLocus R A› isOpen_smoothLocus
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
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, Smooth.{u_2, u_1} R (Localization.Away f)
have refine : FormallySmooth.{u_1, u_2} R (Localization.Away f)
Tactic: refine ⟨f, by simpa using hxf, ⟨?_, inferInstance⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Locus (goal)
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
⊢ FormallySmooth.{u_1, u_2} R (Localization.Away f)
have rwa : ∀ (hf : 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
Cleared hypotheses: hf
-- 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
inst_5 : Finite D.vars
inst_6 : Finite D.rels
⊢ Subalgebra.FG (subalgebra R D)
have 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
Tactic: refine Subalgebra.fg_def.mpr ⟨_, ?_, rfl⟩
-- 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
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
have refine_1 : D.P.coeffs.Finite
Tactic: refine .union ?_ (.union (.union ?_ ?_) ?_)
-- 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
inst_5 : Finite D.vars
inst_6 : Finite D.rels
refine_1 : D.P.coeffs.Finite
⊢ (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
have refine_2 : Set.Finite.{u} (α := A) (⋃ (i : D.vars), (↑(D.h i).coeffs : Set A))
Tactic: refine .union ?_ (.union (.union ?_ ?_) ?_)
-- 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
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))
⊢ (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
have refine_3 : Set.Finite.{u} (α := A) (⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A))
Tactic: refine .union ?_ (.union (.union ?_ ?_) ?_)
-- 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
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))
⊢ (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
have refine_4 : Set.Finite.{u} (α := A) (⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))
Tactic: refine .union ?_ (.union (.union ?_ ?_) ?_)
-- 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
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))
have refine_3 : ∀ (i : D.vars), Set.Finite.{u} (α := A) (⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A))
Tactic: refine Set.finite_iUnion fun i ↦ ?_
-- 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
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))
have refine_4 : ∀ (i : D.rels), Set.Finite.{u} (α := A) (⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A))
Tactic: refine Set.finite_iUnion fun i ↦ ?_
-- 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
⊢ D.P.coeffs ⊆ Set.range (ι := ↥(subalgebra R D)) (⇑(algebraMap (↥(subalgebra R D)) A) : (a : ↥(subalgebra R D)) → A)
have rw : D.P.coeffs ⊆ (↑(subalgebra R D) : Set A)
Tactic: rw [Subalgebra.setRange_algebraMap]
-- 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
D : DescentAux A B
i : D.vars
⊢ (↑(D.h i).coeffs : Set A) ⊆
    Set.range (ι := ↥(subalgebra R D)) (⇑(algebraMap (↥(subalgebra R D)) A) : (a : ↥(subalgebra R D)) → A)
have this : (↑(D.h i).coeffs : Set A) ⊆ ⋃ (i : D.vars), (↑(D.h i).coeffs : Set A)
Tactic: have : ((D.h i).coeffs : Set _) ⊆ ⋃ i, ((D.h i).coeffs : Set A) :=
    Set.subset_iUnion_of_subset i subset_rfl
-- 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
i : D.vars
this : (↑(D.h i).coeffs : Set A) ⊆ ⋃ (i : D.vars), (↑(D.h i).coeffs : Set A)
⊢ (↑(D.h i).coeffs : Set A) ⊆
    Set.range (ι := ↥(subalgebra R D)) (⇑(algebraMap (↥(subalgebra R D)) A) : (a : ↥(subalgebra R D)) → A)
have rw : (↑(D.h i).coeffs : Set A) ⊆ (↑(subalgebra R D) : Set A)
Tactic: rw [Subalgebra.setRange_algebraMap]
-- 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
D : DescentAux A B
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ (↑(D.p i).coeffs : Set (MvPolynomial D.vars A))
⊢ Membership.mem (γ := Set (MvPolynomial D.vars A))
    (Set.range (ι := MvPolynomial D.vars ↥(subalgebra R D))
      (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A))
    p
have this : (↑p.coeffs : Set A) ⊆ ⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A)
Tactic: have : (p.coeffs : Set A) ⊆ ⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs :=
    Set.subset_iUnion_of_subset i (Set.subset_iUnion₂_of_subset p hp subset_rfl)
-- 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
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ (↑(D.p i).coeffs : Set (MvPolynomial D.vars A))
this : (↑p.coeffs : Set A) ⊆ ⋃ (i : D.rels), ⋃ x ∈ (D.p i).coeffs, (↑x.coeffs : Set A)
⊢ Membership.mem (γ := Set (MvPolynomial D.vars A))
    (Set.range (ι := MvPolynomial D.vars ↥(subalgebra R D))
      (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A))
    p
have rw : (↑p.coeffs : Set A) ⊆ (↑(subalgebra R D) : Set A)
Tactic: rw [MvPolynomial.mem_range_map_iff_coeffs_subset, Subalgebra.setRange_algebraMap]
-- 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
D : DescentAux A B
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ (↑(D.q i).coeffs : Set (MvPolynomial D.vars A))
⊢ Membership.mem (γ := Set (MvPolynomial D.vars A))
    (Set.range (ι := MvPolynomial D.vars ↥(subalgebra R D))
      (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A))
    q
have this : (↑q.coeffs : Set A) ⊆ ⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A)
Tactic: have : (q.coeffs : Set A) ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x) :=
    Set.subset_iUnion_of_subset i (Set.subset_iUnion₂_of_subset q hq subset_rfl)
-- 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
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ (↑(D.q i).coeffs : Set (MvPolynomial D.vars A))
this : (↑q.coeffs : Set A) ⊆ ⋃ (i : D.vars), ⋃ x ∈ (D.q i).coeffs, (↑(coeffs x) : Set A)
⊢ Membership.mem (γ := Set (MvPolynomial D.vars A))
    (Set.range (ι := MvPolynomial D.vars ↥(subalgebra R D))
      (⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) :
        (a : MvPolynomial D.vars ↥(subalgebra R D)) → MvPolynomial D.vars A))
    q
have rw : (↑q.coeffs : Set A) ⊆ (↑(subalgebra R D) : Set A)
Tactic: rw [MvPolynomial.mem_range_map_iff_coeffs_subset, Subalgebra.setRange_algebraMap]
-- 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
⊢ ∃ (σ₀ :
    Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
        ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
      MvPolynomial D.vars ↥(subalgebra R D) ⧸
        HPow.hPow (α := Ideal (MvPolynomial D.vars ↥(subalgebra R D))) (β := ℕ)
          (RingHom.ker (F :=
            MvPolynomial D.vars ↥(subalgebra R D) →ₐ[↥(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))))))
          2),
    AlgHom.comp
        (AlgHom.kerSquareLift
          (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))))))
        σ₀ =
      AlgHom.id (↥(subalgebra R D))
        (Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
          ↥(subalgebra R D))
have refine_1 : Presentation.ModelOfHasCoeffs.{u, u_2, 0, 0, u} (R := A) (S := B) (ι := D.vars) (σ := D.rels) (P := D.P)
    ↥(subalgebra R D) →ₐ[↥(subalgebra R D)]
  MvPolynomial D.vars ↥(subalgebra R D) ⧸
    HPow.hPow (α := Ideal (MvPolynomial D.vars ↥(subalgebra R D))) (β := ℕ)
      (RingHom.ker (F :=
        MvPolynomial D.vars ↥(subalgebra R D) →ₐ[↥(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))))))
      2
Tactic: refine ⟨?_, ?_⟩