-- 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 = ⊤
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

Tactic:
apply eq_of_sub_eq_zero

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
⊢ (Ideal.Quotient.mk I) (∑ g : { x // x ∈ s }, g' g * h' g) - 1 = 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 = ⊤
this : Algebra.FinitePresentation R A
g : { x // x ∈ t }
⊢ Algebra.FinitePresentation R (Localization.Away (f' ↑g))

Tactic:
have : ∃ (a : S) (hb : a ∈ s), (Ideal.Quotient.mk I) (g' ⟨a, hb⟩) = g.val := by
  obtain ⟨g, hg⟩ := g
  convert hg
  simp [A, f', t]

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

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

Tactic:
refine Ideal.sum_mem _ (fun g _ ↦ Ideal.mul_mem_right _ _ <| Ideal.subset_span ?_)

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

Proof state:
case h.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
⊢ ∑ g : { x // x ∈ s }, g' g * h' g - 1 ∈ {∑ g : { x // x ∈ s }, g' g * h' g - 1}

Tactic:
simp

Result:
no goals