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)) ⊤
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)
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))
⊢ FinitePresentation.{u_1, u_2} R
    (Localization.Away (M := S) ((Ideal.Quotient.liftₐ I f hfI : (a : A) → S) (↑g : A) : S))

Tactic:
rw [← hrr, Ideal.Quotient.liftₐ_apply, Ideal.Quotient.lift_mk]

Premises used: Ideal.Quotient.lift_mk, Ideal.Quotient.liftₐ_apply
-- 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_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))
⊢ 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:
simp_rw +instances [RingHom.coe_coe]

Premises used: RingHom.coe_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
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)
rw : FinitePresentation.{u_1, u_2} R (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))
⊢ 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:
rw [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 : ↥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 (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))

Tactic:
apply h
-- 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), 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
-- 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
Ht : ∀ (g : ↥t), FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f' : (a : A) → S) (↑g : A) : S))
⊢ FinitePresentation R S

Tactic:
of_span_eq_top_target_aux f' hf' t ht Ht

Premises used: Algebra.FinitePresentation.of_span_eq_top_target_aux
-- 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
Ht : ∀ (g : ↥t), FinitePresentation.{u_1, u_2} R (Localization.Away (M := S) ((f' : (a : A) → S) (↑g : A) : S))
⊢ FinitePresentation R S

Tactic:
exact of_span_eq_top_target_aux f' hf' t ht Ht

Premises used: Algebra.FinitePresentation.of_span_eq_top_target_aux
-- 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
ι : 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)
apply : ∀ i ∈ Set.range s, FinitePresentation.{u_1, u_2} R (Localization.Away i)
⊢ FinitePresentation R S

Tactic:
apply of_span_eq_top_target _ hs

Premises used: Algebra.FinitePresentation.of_span_eq_top_target
-- 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
ι : 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)
i : ι
⊢ FinitePresentation.{u_1, u_2} R (Localization.Away (s i))

Tactic:
.equiv <| (IsLocalization.algEquiv (.powers <| s i) _ (T i)).symm |>.restrictScalars R

Premises used: Algebra.FinitePresentation.equiv, AlgEquiv.symm, AlgEquiv.restrictScalars, IsLocalization.algEquiv, Submonoid.powers
-- 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
ι : 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)
i : ι
⊢ FinitePresentation.{u_1, u_2} R (Localization.Away (s i))

Tactic:
exact .equiv <| (IsLocalization.algEquiv (.powers <| s i) _ (T i)).symm |>.restrictScalars R

Premises used: AlgEquiv.symm, AlgEquiv.restrictScalars, IsLocalization.algEquiv, Submonoid.powers
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
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)

Tactic:
IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
      ((Pi.evalRingHom S i).surjective)

Premises used: RingHom.ker_evalRingHom, IsLocalization.away_of_isIdempotentElem, Pi.evalRingHom, RingHom.surjective
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
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 : ι
refine : IsIdempotentElem (M := (j : ι) → S j) (Pi.single (M := S) i 1)
⊢ IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)

Tactic:
refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
      ((Pi.evalRingHom S i).surjective)

Premises used: IsLocalization.away_of_isIdempotentElem, Pi.evalRingHom, RingHom.surjective
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
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 : ι
⊢ IsIdempotentElem (M := (j : ι) → S j) (Pi.single (M := S) i 1)

Tactic:
simp [IsIdempotentElem, ← Pi.single_mul_left]

Premises used: IsIdempotentElem, Pi.single_mul_left
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
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)

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]
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
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_1 : (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:
Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
    _ (Ideal.span_single_eq_top S) (fun i ↦ S i)

Premises used: Ideal.span_single_eq_top, Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
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_1 : (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:
exact Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
    _ (Ideal.span_single_eq_top S) (fun i ↦ S i)

Premises used: Ideal.span_single_eq_top, Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
-- Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal
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)
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)
⊢ 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)