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

Proof state:
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

Tactic:
letI := f.toAlgebra

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
this : Algebra R S := f.toAlgebra
⊢ f.FinitePresentation

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 = ⊤
this✝ : Algebra.FinitePresentation R A
g : { x // x ∈ t }
this : ∃ a, ∃ (hb : a ∈ s), (Ideal.Quotient.mk I) (g' ⟨a, hb⟩) = ↑g
⊢ Algebra.FinitePresentation R (Localization.Away (f' ↑g))

Tactic:
obtain ⟨r, hr, hrr⟩ := this

Result:
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 (f' ↑g))

Proof state:
case h.e'_5.h.h
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 }), Algebra.FinitePresentation R (Localization.Away ↑r)
this : Algebra R S := f.toAlgebra
r : { x // x ∈ s }
e_4✝ : OreLocalization.instSemiring = CommSemiring.toSemiring
r✝ : R
x✝ : OreLocalization (Submonoid.powers ↑r) S
⊢ (algebraMap R (OreLocalization (Submonoid.powers ↑r) S)) r✝ * x✝ =
    (algebraMap R (OreLocalization (Submonoid.powers ↑r) S)) r✝ * x✝

Tactic:
rfl

Result:
no goals

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
⊢ (Ideal.Quotient.mk I) (∑ g : { x // x ∈ s }, g' g * h' g) - 1 = 0

Tactic:
rw [← map_one (Ideal.Quotient.mk I), ← map_sub, Ideal.Quotient.eq_zero_iff_mem]

Result:
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
⊢ ∑ g : { x // x ∈ s }, g' g * h' g - 1 ∈ I