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

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 (↑f (g' ⟨r, hr⟩)))

Tactic:
simp_rw [coe_coe]

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' ⟨r, hr⟩)))

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

Tactic:
let f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI

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

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 ((Ideal.Quotient.liftₐ I f hfI) ↑g))

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

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' ⟨r, hr⟩)))

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

Tactic:
choose h' hh' using (fun g : s ↦ hf (l g))

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