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

Proof state:
case mk
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 = ⊤
this : Algebra.FinitePresentation R A
g : A
hg : g ∈ t
⊢ ∃ a, ∃ (hb : a ∈ s), (Ideal.Quotient.mk I) (g' ⟨a, hb⟩) = ↑⟨g, hg⟩

Tactic:
convert hg

Result:
case a
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 = ⊤
this : Algebra.FinitePresentation R A
g : A
hg : g ∈ t
⊢ (∃ a, ∃ (hb : a ∈ s), (Ideal.Quotient.mk I) (g' ⟨a, hb⟩) = ↑⟨g, hg⟩) ↔ g ∈ t

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 : ∑ i ∈ s.attach, l i • ↑i = 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
⊢ (∑ x ∈ s.attach, ↑x * l x - 1) * f q = 0

Tactic:
rw [← hl]

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 : ∑ i ∈ s.attach, l i • ↑i = 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
⊢ (∑ x ∈ s.attach, ↑x * l x - ∑ i ∈ s.attach, l i • ↑i) * f q = 0

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
ht : Ideal.span ↑t = ⊤
⊢ Ideal.span ↑{∑ g ∈ s.attach, g' g * h' g - 1} = Ideal.span {∑ g ∈ s.attach, g' g * h' g - 1}

Tactic:
simp

Result:
no goals

Proof state:
case 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}
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 = ⊤
this : Algebra.FinitePresentation R A
g : { x // x ∈ t }
r : S
hr : r ∈ s
hrr : (Ideal.Quotient.mk I) (g' ⟨r, hr⟩) = ↑g
⊢ Algebra.FinitePresentation R (Localization.Away ↑⟨r, hr⟩)

Tactic:
apply H

Result:
no goals

Proof state:
case 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
⊢ Algebra.FinitePresentation R S

Tactic:
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)

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
⊢ Algebra.FinitePresentation R S