awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
h₂ :
  HSub.hSub (α := MvPolynomial (Fin n) R ⧸ I)
      ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1 =
    0
⊢ Eq (α := MvPolynomial (Fin n) R ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1

Tactic:
apply eq_of_sub_eq_zero

Premises used: eq_of_sub_eq_zero
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
h₂ : HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1 ∈ I
⊢ HSub.hSub (α := MvPolynomial (Fin n) R ⧸ I)
      ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1 =
    0

Tactic:
rw [← map_one (Ideal.Quotient.mk I), ← map_sub, Ideal.Quotient.eq_zero_iff_mem]

Premises used: map_sub, Ideal.Quotient.mk, Ideal.Quotient.eq_zero_iff_mem, map_one
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
h₂ :
  Membership.mem (γ := Set (MvPolynomial (Fin n) R)) {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
    (HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1)
⊢ HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1 ∈ I

Tactic:
apply Ideal.subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
⊢ Membership.mem (γ := Set (MvPolynomial (Fin n) R)) {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
    (HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
⊢ Eq (α := MvPolynomial (Fin n) R ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1

Tactic:
have : ∑ g : { x // x ∈ s }, g' g * h' g = (1 : A) := by
      apply eq_of_sub_eq_zero
      rw [← map_one (Ideal.Quotient.mk I), ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
      apply Ideal.subset_span
      simp
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
this :
  Eq (α := MvPolynomial (Fin n) R ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1
simp_rw :
  Membership.mem (γ := Ideal A) (Ideal.span (↑t : Set A))
    (∑ x ∈ s.attach,
      HMul.hMul (α := MvPolynomial (Fin n) R ⧸ I) (β := MvPolynomial (Fin n) R ⧸ I)
        ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' x) :
          MvPolynomial (Fin n) R ⧸ I)
        ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (h' x) :
          MvPolynomial (Fin n) R ⧸ I))
⊢ Membership.mem (γ := Ideal A) (Ideal.span (↑t : Set A)) 1

Tactic:
simp_rw [← this, Finset.univ_eq_attach, map_sum, map_mul]

Premises used: map_sum, map_mul, Finset.univ_eq_attach
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
this :
  Eq (α := MvPolynomial (Fin n) R ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1
⊢ Membership.mem (γ := Ideal A) (Ideal.span (↑t : Set A))
    (∑ x ∈ s.attach,
      HMul.hMul (α := MvPolynomial (Fin n) R ⧸ I) (β := MvPolynomial (Fin n) R ⧸ I)
        ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' x) :
          MvPolynomial (Fin n) R ⧸ I)
        ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (h' x) :
          MvPolynomial (Fin n) R ⧸ I))

Tactic:
Ideal.sum_mem _ (fun g _ ↦ Ideal.mul_mem_right _ _ <| Ideal.subset_span ?_)

Premises used: Ideal.subset_span, Set.Mem, Ideal.Quotient.mk, Ideal.sum_mem, SetLike.coe, Ideal.mul_mem_right, Ideal.span, DFunLike.coe
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
this :
  Eq (α := MvPolynomial (Fin n) R ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1
refine :
  ∀ g ∈ s.attach,
    Membership.mem (α := A) (↑t : Set A)
      ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g) :
        MvPolynomial (Fin n) R ⧸ I)
⊢ Membership.mem (γ := Ideal A) (Ideal.span (↑t : Set A))
    (∑ x ∈ s.attach,
      HMul.hMul (α := MvPolynomial (Fin n) R ⧸ I) (β := MvPolynomial (Fin n) R ⧸ I)
        ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' x) :
          MvPolynomial (Fin n) R ⧸ I)
        ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (h' x) :
          MvPolynomial (Fin n) R ⧸ I))

Tactic:
refine Ideal.sum_mem _ (fun g _ ↦ Ideal.mul_mem_right _ _ <| Ideal.subset_span ?_)

Premises used: Ideal.subset_span, Ideal.sum_mem, Ideal.mul_mem_right, Ideal.span
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
this :
  Eq (α := MvPolynomial (Fin n) R ⧸ I)
    ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (∑ g : ↥s, g' g * h' g)) 1
g : ↥s
h_1 : g ∈ s.attach
⊢ Membership.mem (α := A) (↑t : Set A)
    ((Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g) :
      MvPolynomial (Fin n) R ⧸ I)

Tactic:
simp [t]
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
⊢ Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤

Tactic:
have ht : Ideal.span (t : Set A) = ⊤ := by
    rw [Ideal.eq_top_iff_one]
    have : ∑ g : { x // x ∈ s }, g' g * h' g = (1 : A) := by
      apply eq_of_sub_eq_zero
      rw [← map_one (Ideal.Quotient.mk I), ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
      apply Ideal.subset_span
      simp
    simp_rw [← this, Finset.univ_eq_attach, map_sum, map_mul]
    refine Ideal.sum_mem _ (fun g _ ↦ Ideal.mul_mem_right _ _ <| Ideal.subset_span ?_)
    simp [t]
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s_1 : Set S
hs_1 : Eq (α := Ideal S) (Ideal.span s_1) ⊤
s : Finset S
h₁ : (↑s : Set S) ⊆ s_1
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
h : ∀ (i : ↥s), FinitePresentation.{u_1, u_2} R (Localization.Away (↑i : S))
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
l : (↑(↑s : Set S) : Type u_2) →₀ S
hl :
  Eq (α := S)
    ((Finsupp.linearCombination S (Subtype.val (p := fun (x : S) ↦ x ∈ (↑s : Set S))) :
          (a : (↑(↑s : Set S) : Type u_2) →₀ S) → S)
        l :
      S)
    (1 : S)
g' : (g : ↥s) → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), (f : (a : MvPolynomial (Fin n) R) → S) (g' g) = (↑g : S)
h' : (g : ↥s) → MvPolynomial (Fin n) R
hh' :
  ∀ (g : ↥s),
    Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (h' g) : S)
      ((l : (a : (↑(↑s : Set S) : Type u_2)) → S) g : S)
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g : ↥s, g' g * h' g) 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) a : S) (0 : S)
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := S) (⇑f' : (a : A) → S)
t : Finset A :=
  Finset.image (fun (g : ↥s) ↦ (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I) (g' g))
    Finset.univ
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
h₂ : I.FG
⊢ FinitePresentation R A

Tactic:
apply Algebra.FinitePresentation.quotient

Premises used: Algebra.FinitePresentation.quotient