-- Mathlib/RingTheory/RingHom/FinitePresentation.lean
theorem finitePresentation_ofLocalizationSpanTarget :
    OfLocalizationSpanTarget @FinitePresentation

Proof state:
case intro.intro.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f✝.toAlgebra
H : ∀ (r : { x // x ∈ s }), Algebra.FinitePresentation R (Localization.Away ↑r)
hfintype : Algebra.FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : { x // x ∈ s } → MvPolynomial (Fin n) R
hg' : ∀ (g : { x // x ∈ s }), f (g' g) = ↑g
h' : { x // x ∈ s } → MvPolynomial (Fin n) R
hh' : ∀ (g : { x // x ∈ s }), f (h' g) = l g
⊢ Algebra.FinitePresentation R S

Tactic:
let I : Ideal (MvPolynomial (Fin n) R) := Ideal.span { ∑ g : s, g' g * h' g - 1 }

Result:
case intro.intro.intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f✝.toAlgebra
H : ∀ (r : { x // x ∈ s }), Algebra.FinitePresentation R (Localization.Away ↑r)
hfintype : Algebra.FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : { x // x ∈ s } → MvPolynomial (Fin n) R
hg' : ∀ (g : { x // x ∈ s }), f (g' g) = ↑g
h' : { x // x ∈ s } → MvPolynomial (Fin n) R
hh' : ∀ (g : { x // x ∈ s }), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g : { x // x ∈ s }, g' g * h' g - 1}
⊢ Algebra.FinitePresentation R S

Proof state:
⊢ OfLocalizationFiniteSpanTarget @FinitePresentation

Tactic:
introv R hs H

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), ((algebraMap S (Localization.Away ↑r)).comp f).FinitePresentation
⊢ f.FinitePresentation

Proof state:
case intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f✝.toAlgebra
H : ∀ (r : { x // x ∈ s }), Algebra.FinitePresentation R (Localization.Away ↑r)
hfintype : Algebra.FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : { x // x ∈ s } → MvPolynomial (Fin n) R
hg' : ∀ (g : { x // x ∈ s }), f (g' g) = ↑g
h' : { x // x ∈ s } → MvPolynomial (Fin n) R
hh' : ∀ (g : { x // x ∈ s }), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g : { x // x ∈ s }, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ l ∈ Finsupp.supported S S ↑s.attach

Tactic:
rintro a -

Result:
case intro
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f✝.toAlgebra
H : ∀ (r : { x // x ∈ s }), Algebra.FinitePresentation R (Localization.Away ↑r)
hfintype : Algebra.FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : { x // x ∈ s } → MvPolynomial (Fin n) R
hg' : ∀ (g : { x // x ∈ s }), f (g' g) = ↑g
h' : { x // x ∈ s } → MvPolynomial (Fin n) R
hh' : ∀ (g : { x // x ∈ s }), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g : { x // x ∈ s }, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
a : { x // x ∈ s }
⊢ a ∈ ↑s.attach

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f✝.toAlgebra
H : ∀ (r : { x // x ∈ s }), Algebra.FinitePresentation R (Localization.Away ↑r)
hfintype : Algebra.FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : { x // x ∈ s } → MvPolynomial (Fin n) R
hg' : ∀ (g : { x // x ∈ s }), f (g' g) = ↑g
h' : { x // x ∈ s } → MvPolynomial (Fin n) R
hh' : ∀ (g : { x // x ∈ s }), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g : { x // x ∈ s }, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g => (Ideal.Quotient.mk I) (g' g)) Finset.univ
⊢ Ideal.span ↑t = ⊤

Tactic:
rw [Ideal.eq_top_iff_one]

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f✝.toAlgebra
H : ∀ (r : { x // x ∈ s }), Algebra.FinitePresentation R (Localization.Away ↑r)
hfintype : Algebra.FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : { x // x ∈ s } → MvPolynomial (Fin n) R
hg' : ∀ (g : { x // x ∈ s }), f (g' g) = ↑g
h' : { x // x ∈ s } → MvPolynomial (Fin n) R
hh' : ∀ (g : { x // x ∈ s }), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g : { x // x ∈ s }, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g => (Ideal.Quotient.mk I) (g' g)) Finset.univ
⊢ 1 ∈ Ideal.span ↑t

Proof state:
case h
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R →+* S
s : Finset S
hs : Ideal.span ↑s = ⊤
this : Algebra R S := f✝.toAlgebra
H : ∀ (r : { x // x ∈ s }), Algebra.FinitePresentation R (Localization.Away ↑r)
hfintype : Algebra.FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : { x // x ∈ s } → MvPolynomial (Fin n) R
hg' : ∀ (g : { x // x ∈ s }), f (g' g) = ↑g
h' : { x // x ∈ s } → MvPolynomial (Fin n) R
hh' : ∀ (g : { x // x ∈ s }), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g : { x // x ∈ s }, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
hfI : ∀ a ∈ I, f a = 0
f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
hf' : Function.Surjective ⇑f'
t : Finset A := Finset.image (fun g => (Ideal.Quotient.mk I) (g' g)) Finset.univ
ht : Ideal.span ↑t = ⊤
⊢ (Ideal.span {∑ g ∈ s.attach, g' g * h' g - 1}).FG

Tactic:
exact ⟨{∑ g ∈ s.attach, g' g * h' g - 1}, by simp⟩

Result:
no goals