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
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
h₂ :
  Ideal.FG (R := MvPolynomial (Fin n) R)
    (Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g ∈ s.attach, g' g * h' g) 1})
⊢ I.FG

Tactic:
simp only [Finset.univ_eq_attach, I]

Premises used: 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
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.span
      (↑{HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g ∈ s.attach, g' g * h' g) 1} : Set (MvPolynomial (Fin n) R)))
    (Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g ∈ s.attach, 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
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
⊢ Ideal.FG (R := MvPolynomial (Fin n) R)
    (Ideal.span {HSub.hSub (α := MvPolynomial (Fin n) R) (∑ g ∈ s.attach, g' g * h' g) 1})

Tactic:
exact ⟨{∑ g ∈ s.attach, g' g * h' g - 1}, by 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
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
⊢ FinitePresentation R A

Tactic:
have : Algebra.FinitePresentation R A := by
    apply Algebra.FinitePresentation.quotient
    simp only [Finset.univ_eq_attach, I]
    exact ⟨{∑ g ∈ s.attach, g' g * h' g - 1}, by 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
ht : Eq (α := Ideal A) (Ideal.span (↑t : Set A)) ⊤
this : FinitePresentation R A
g : ↥t
obtain :
  ∀ (g : A) (hg : g ∈ t),
    ∃ (a : S) (hb : a ∈ s),
      (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I)
          (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) a hb)) =
        (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ t) g hg) : A)
⊢ ∃ (a : S) (hb : a ∈ s),
    (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I)
        (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) a hb)) =
      (↑g : A)

Tactic:
obtain ⟨g, hg⟩ := g
-- 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)) ⊤
this : FinitePresentation R A
g : A
hg : g ∈ t
⊢ g ∈ t

Tactic:
hg
-- 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)) ⊤
this : FinitePresentation R A
g : A
hg : g ∈ t
a :
  (∃ (a : S) (hb : a ∈ s),
      (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I)
          (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) a hb)) =
        (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ t) g hg) : A)) ↔
    g ∈ t
⊢ ∃ (a : S) (hb : a ∈ s),
    (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I)
        (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) a hb)) =
      (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ t) g hg) : A)

Tactic:
convert! hg
-- 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)) ⊤
this : FinitePresentation R A
g : A
hg : g ∈ t
⊢ (∃ (a : S) (hb : a ∈ s),
      (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I)
          (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) a hb)) =
        (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ t) g hg) : A)) ↔
    g ∈ t

Tactic:
simp [A, 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)) ⊤
this : FinitePresentation R A
g : ↥t
⊢ ∃ (a : S) (hb : a ∈ s),
    (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I)
        (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) a hb)) =
      (↑g : A)

Tactic:
have : ∃ (a : S) (hb : a ∈ s), (Ideal.Quotient.mk I) (g' ⟨a, hb⟩) = g.val := by
      obtain ⟨g, hg⟩ := g
      convert! hg
      simp [A, 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)) ⊤
this_1 : FinitePresentation R A
g : ↥t
this :
  ∃ (a : S) (hb : a ∈ s),
    (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I)
        (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) a hb)) =
      (↑g : A)
obtain :
  ∀ (r : S) (hr : r ∈ s)
    (hrr :
      (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I)
          (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr)) =
        (↑g : A)),
    FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f' : (a : A) → S) (↑g : A) : S))
⊢ FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f' : (a : A) → S) (↑g : A) : S))

Tactic:
obtain ⟨r, hr, hrr⟩ := this
-- 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)) ⊤
this : FinitePresentation R A
g : ↥t
r : S
hr : r ∈ s
hrr :
  (Ideal.Quotient.mk I : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) R ⧸ I)
      (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr)) =
    (↑g : A)
simp :
  FinitePresentation.{u_1, u_2} R
    (Localization.Away (M := S) ((Ideal.Quotient.liftₐ I f hfI : (a : A) → S) (↑g : A) : S))
⊢ FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f' : (a : A) → S) (↑g : A) : S))

Tactic:
simp only [f']