-- Mathlib/RingTheory/FinitePresentation.lean
theorem of_finiteType [IsNoetherianRing R] : FiniteType R A ↔ FinitePresentation R A

Proof state:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
⊢ FiniteType R A ↔ FinitePresentation R A

Tactic:
refine ⟨fun h => ?_, fun hfp => Algebra.FiniteType.of_finitePresentation⟩

Result:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
⊢ FinitePresentation R A

Proof state:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
letI : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule

Result:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
this : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule
⊢ (RingHom.ker f.toRingHom).FG

Proof state:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
⊢ FinitePresentation R A

Tactic:
obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.1 h

Result:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
⊢ FinitePresentation R A

Proof state:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
⊢ FinitePresentation R A

Tactic:
refine ⟨n, f, hf, ?_⟩

Result:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
⊢ (RingHom.ker f.toRingHom).FG

Proof state:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
⊢ IsNoetherianRing (MvPolynomial (Fin n) R)

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
this : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
convert hnoet.noetherian (RingHom.ker f.toRingHom)

Result:
no goals

Proof state:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
hnoet : IsNoetherianRing (MvPolynomial (Fin n) R)
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
rw [isNoetherianRing_iff] at hnoet

Result:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
⊢ (RingHom.ker f.toRingHom).FG

Proof state:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
have hnoet : IsNoetherianRing (MvPolynomial (Fin n) R) := by infer_instance

Result:
case intro.intro
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
hnoet : IsNoetherianRing (MvPolynomial (Fin n) R)
⊢ (RingHom.ker f.toRingHom).FG