awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
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
⊢ FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f' : (a : A) → S) (↑g : A) : S))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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)
⊢ FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f' : (a : A) → S) (↑g : A) : S))
have 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))
Tactic: obtain ⟨r, hr, hrr⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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)
⊢ FinitePresentation.{u_1, u_2} R
    (Localization.Away (M := S) ((Ideal.Quotient.liftₐ I f hfI : (a : A) → S) (↑g : A) : S))
have rw : FinitePresentation.{u_1, u_2} R
  (Localization.Away (M := S)
    (((↑f : MvPolynomial (Fin n) R →+* S) : (a : MvPolynomial (Fin n) R) → S)
        (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr)) :
      S))
Tactic: rw [← hrr, Ideal.Quotient.liftₐ_apply, Ideal.Quotient.lift_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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)
⊢ FinitePresentation.{u_1, u_2} R
    (Localization.Away (M := S)
      (((↑f : MvPolynomial (Fin n) R →+* S) : (a : MvPolynomial (Fin n) R) → S)
          (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr)) :
        S))
have simp_rw : FinitePresentation.{u_1, u_2} R
  (Localization.Away (M := S)
    ((f : (a : MvPolynomial (Fin n) R) → S) (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr)) : S))
Tactic: simp_rw +instances [RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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)
⊢ FinitePresentation.{u_1, u_2} R
    (Localization.Away (M := S)
      ((f : (a : MvPolynomial (Fin n) R) → S) (g' (Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr)) : S))
have rw : FinitePresentation.{u_1, u_2} R (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))
Tactic: rw [hg']
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
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
⊢ FinitePresentation R S
have Ht : ∀ (g : ↥t), FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f' : (a : A) → S) (↑g : A) : S))
Tactic: have Ht (g : t) : Algebra.FinitePresentation R (Localization.Away (f' g)) := by
    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]
    obtain ⟨r, hr, hrr⟩ := this
    simp only [f']
    rw [← hrr, Ideal.Quotient.liftₐ_apply, Ideal.Quotient.lift_mk]
    simp_rw +instances [RingHom.coe_coe]
    rw [hg']
    apply h
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
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))
⊢ FinitePresentation R S
have We : FiniteType R S
Tactic: classical
  /-
  We already know that `S` is of finite type over `R`, so we have a surjection
  `MvPolynomial (Fin n) R →ₐ[R] S`. To reason about the kernel, we want to check it on the stalks
  of preimages of `s`. But the preimages do not necessarily span `MvPolynomial (Fin n) R`, so
  we quotient out by an ideal and apply `finitePresentation_ofLocalizationSpanTarget_aux`.
  -/
  have hfintype : Algebra.FiniteType R S := by
    apply Algebra.FiniteType.of_span_eq_top_target s hs
    intro x hx
    have := h ⟨x, hx⟩
    infer_instance
  obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp hfintype
  obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_linearCombination S (s : Set S) 1).mp
      (show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
  choose g' hg' using (fun g : s ↦ hf g)
  choose h' hh' using (fun g : s ↦ hf (l g))
  let I : Ideal (MvPolynomial (Fin n) R) := Ideal.span { ∑ g : s, g' g * h' g - 1 }
  let A := MvPolynomial (Fin n) R ⧸ I
  have hfI : ∀ a ∈ I, f a = 0 := by
    intro p hp
    simp only [Finset.univ_eq_attach, I, Ideal.mem_span_singleton] at hp
    obtain ⟨q, rfl⟩ := hp
    simp only [map_mul, map_sub, map_sum, map_one, hg', hh']
    rw [Finsupp.linearCombination_apply_of_mem_supported (α := (s : Set S)) S (s := s.attach)] at hl
    · rw [← hl]
      simp only [Finset.coe_sort_coe, smul_eq_mul, mul_comm, sub_self, zero_mul]
    · rintro a -
      simp
  let f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
  have hf' : Function.Surjective f' :=
    Ideal.Quotient.lift_surjective_of_surjective I hfI hf
  let t : Finset A := Finset.image (fun g ↦ g' g) Finset.univ
  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]
  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⟩
  have Ht (g : t) : Algebra.FinitePresentation R (Localization.Away (f' g)) := by
    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]
    obtain ⟨r, hr, hrr⟩ := this
    simp only [f']
    rw [← hrr, Ideal.Quotient.liftₐ_apply, Ideal.Quotient.lift_mk]
    simp_rw +instances [RingHom.coe_coe]
    rw [hg']
    apply h
  exact of_span_eq_top_target_aux f' hf' t ht Ht
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type u_3
s : ι → S
hs : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤
T : ι → Type u_4
inst_3 : (i : ι) → CommRing (T i)
inst_4 : (i : ι) → Algebra.{u_1, u_4} R (T i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} S (T i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_4} R S (T i)
inst_7 : ∀ (i : ι), IsLocalization.Away.{u_2, u_4} (s i) (T i)
inst_8 : ∀ (i : ι), FinitePresentation.{u_1, u_4} R (T i)
⊢ FinitePresentation R S
have apply : ∀ i ∈ Set.range s, FinitePresentation.{u_1, u_2} R (Localization.Away i)
Tactic: apply of_span_eq_top_target _ hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommRing R
inst_1 : CommRing S_1
inst_2 : Algebra R S_1
ι : Type u_3
inst_3 : Finite ι
S : ι → Type u_4
inst_4 : (i : ι) → CommRing (S i)
inst_5 : (i : ι) → Algebra.{u_1, u_4} R (S i)
inst_6 : ∀ (i : ι), FinitePresentation.{u_1, u_4} R (S i)
this : (i : ι) → Algebra ((a : ι) → S a) (S i) :=
  fun (i : ι) ↦ RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i))
i : ι
⊢ IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)
have refine : IsIdempotentElem (M := (j : ι) → S j) (Pi.single (M := S) i 1)
Tactic: refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
      ((Pi.evalRingHom S i).surjective)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (hypothesis)
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommRing R
inst_1 : CommRing S_1
inst_2 : Algebra R S_1
ι : Type u_3
inst_3 : Finite ι
S : ι → Type u_4
inst_4 : (i : ι) → CommRing (S i)
inst_5 : (i : ι) → Algebra.{u_1, u_4} R (S i)
inst_6 : ∀ (i : ι), FinitePresentation.{u_1, u_4} R (S i)
this : (i : ι) → Algebra ((a : ι) → S a) (S i) :=
  fun (i : ι) ↦ RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i))
⊢ FinitePresentation R ((a : ι) → S a)
have this₁ : ∀ (i : ι), IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)
Tactic: have (i : ι) : IsLocalization.Away (Pi.single i 1 : ∀ a, S a) (S i) := by
    refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
      ((Pi.evalRingHom S i).surjective)
    simp [IsIdempotentElem, ← Pi.single_mul_left]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FinitePresentationLocal (goal)
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommRing R
inst_1 : CommRing S_1
inst_2 : Algebra R S_1
ι : Type u_3
inst_3 : Finite ι
S : ι → Type u_4
inst_4 : (i : ι) → CommRing (S i)
inst_5 : (i : ι) → Algebra.{u_1, u_4} R (S i)
inst_6 : ∀ (i : ι), FinitePresentation.{u_1, u_4} R (S i)
let let₁ let₂ : FinitePresentation R ((a : ι) → S a)
⊢ FinitePresentation R ((a : ι) → S a)
have let₃ : let this : (i : ι) → Algebra ((a : ι) → S a) (S i) := fun (i : ι) ↦
  RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i));
∀ (this : ∀ (i : ι), IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)),
  FinitePresentation R ((a : ι) → S a)
Tactic: classical
  let (i : ι) : Algebra (Π a, S a) (S i) := (Pi.evalAlgHom R S i).toAlgebra
  have (i : ι) : IsLocalization.Away (Pi.single i 1 : ∀ a, S a) (S i) := by
    refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
      ((Pi.evalRingHom S i).surjective)
    simp [IsIdempotentElem, ← Pi.single_mul_left]
  exact Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
    _ (Ideal.span_single_eq_top S) (fun i ↦ S i)
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
⊢ ∃ (m : ↥M), m • x ∈ A
have hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
Tactic: have hx₁ : (y : S) • (s : Set S') = g '' _ :=
    (IsLocalization.finsetIntegerMultiple_image _ s).symm
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
⊢ (↑y : S) • (↑s : Set S') ⊆ (↑(Subalgebra.map g A) : Set S')
have rw : (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑(Subalgebra.map g A) : Set S')
Tactic: rw [hx₁]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.FiniteTypeLocal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
S' : Type u_4
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
M : Submonoid S
inst_7 : IsLocalization M S'
x : S
s : Finset S'
A : Subalgebra R S
hA₁ : (↑(finsetIntegerMultiple M s) : Set S) ⊆ (↑A : Set S)
hA₂ : M ≤ A.toSubmonoid
hx :
  Membership.mem (α := S') (γ := Subalgebra R S') (Algebra.adjoin R (↑s : Set S'))
    ((algebraMap S S' : (a : S) → S') x : S')
g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'
y : ↥M := commonDenomOfFinset M s
hx₁ : (↑y : S) • (↑s : Set S') = (⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple M s) : Set S)
⊢ ∃ (m : ↥M), m • x ∈ A
have obtain : ∀ (n : ℕ)
  (hn :
    ∀ n_1 ≥ n, HSMul.hSMul (β := S') ((↑y : S) ^ n_1) ((algebraMap S S' : (a : S) → S') x : S') ∈ Subalgebra.map g A),
  ∃ (m : ↥M), m • x ∈ A
Tactic: obtain ⟨n, hn⟩ :=
    Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin (y : S) (s : Set S') (A.map g)
      (by rw [hx₁]; exact Set.image_mono hA₁) hx (Set.mem_image_of_mem _ (hA₂ y.2))