-- Mathlib/RingTheory/RingHom/FinitePresentation.lean
/--
If `S` is an `R`-algebra with a surjection from a finitely-presented `R`-algebra `A`, such that
localized at a spanning set `{ r }` of elements of `A`, `Sᵣ` is finitely-presented, then
`S` is finitely presented.
This is almost `finitePresentation_ofLocalizationSpanTarget`. The difference is,
that here the set `t` generates the unit ideal of `A`, while in the general version,
it only generates a quotient of `A`.
-/
lemma finitePresentation_ofLocalizationSpanTarget_aux
    {R S A : Type*} [CommRing R] [CommRing S] [CommRing A] [Algebra R S] [Algebra R A]
    [Algebra.FinitePresentation R A] (f : A →ₐ[R] S) (hf : Function.Surjective f)
    (t : Finset A) (ht : Ideal.span (t : Set A) = ⊤)
    (H : ∀ g : t, Algebra.FinitePresentation R (Localization.Away (f g))) :
    Algebra.FinitePresentation R S

Proof state:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
g : ↑↑t
f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := Localization.awayMapₐ f ↑g
⊢ (ker (Localization.awayMap f.toRingHom ↑g)).FG

Tactic:
have (g : t) : Algebra.FinitePresentation R (Localization.Away g.val) :=
  haveI : Algebra.FinitePresentation A (Localization.Away g.val) :=
    IsLocalization.Away.finitePresentation g.val
  Algebra.FinitePresentation.trans R A (Localization.Away g.val)

Result:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
g : ↑↑t
f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := Localization.awayMapₐ f ↑g
this : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away ↑g)
⊢ (ker (Localization.awayMap f.toRingHom ↑g)).FG

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
⊢ Algebra.FinitePresentation R S

Tactic:
apply Algebra.FinitePresentation.of_surjective hf

Result:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
⊢ (ker f.toRingHom).FG

Proof state:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
⊢ ∀ (g : ↑↑t), (ker (Localization.awayMap f.toRingHom ↑g)).FG

Tactic:
intro g

Result:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
g : ↑↑t
⊢ (ker (Localization.awayMap f.toRingHom ↑g)).FG

Proof state:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
⊢ (ker f.toRingHom).FG

Tactic:
apply ker_fg_of_localizationSpan t ht

Result:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
⊢ ∀ (g : ↑↑t), (ker (Localization.awayMap f.toRingHom ↑g)).FG

Proof state:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
g : ↑↑t
⊢ (ker (Localization.awayMap f.toRingHom ↑g)).FG

Tactic:
let f' : Localization.Away g.val →ₐ[R] Localization.Away (f g) :=
  Localization.awayMapₐ f g.val

Result:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
g : ↑↑t
f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := Localization.awayMapₐ f ↑g
⊢ (ker (Localization.awayMap f.toRingHom ↑g)).FG

Proof state:
case hker.hf
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
g : ↑↑t
f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := Localization.awayMapₐ f ↑g
this : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away ↑g)
⊢ Function.Surjective ⇑f'

Tactic:
exact IsLocalization.Away.mapₐ_surjective_of_surjective _ hf

Result:
no goals

Proof state:
case hker
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
g : ↑↑t
f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := Localization.awayMapₐ f ↑g
this : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away ↑g)
⊢ (ker (Localization.awayMap f.toRingHom ↑g)).FG

Tactic:
apply Algebra.FinitePresentation.ker_fG_of_surjective f'

Result:
case hker.hf
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra.FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))
g : ↑↑t
f' : Localization.Away ↑g →ₐ[R] Localization.Away (f ↑g) := Localization.awayMapₐ f ↑g
this : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away ↑g)
⊢ Function.Surjective ⇑f'