-- Mathlib/RingTheory/Jacobson/Ring.lean
@[stacks 0CY7 "See also https://en.wikipedia.org/wiki/Zariski%27s_lemma."]
lemma finite_of_finite_type_of_isJacobsonRing (R S : Type*) [CommRing R] [Field S]
    [Algebra R S] [IsJacobsonRing R] [Algebra.FiniteType R S] :
    Module.Finite R S

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
⊢ Module.Finite R S

Tactic:
obtain ⟨ι, hι, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial'.mp ‹_›

Result:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ Module.Finite R S

Proof state:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
this : (algebraMap R S).IsIntegral
⊢ Module.Finite R S

Tactic:
have : Algebra.IsIntegral R S := Algebra.isIntegral_def.mpr this

Result:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
this✝ : (algebraMap R S).IsIntegral
this : Algebra.IsIntegral R S
⊢ Module.Finite R S

Proof state:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
this✝ : (algebraMap R S).IsIntegral
this : Algebra.IsIntegral R S
⊢ Module.Finite R S

Tactic:
exact Algebra.IsIntegral.finite

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ (algebraMap R S).IsIntegral

Tactic:
rw [← f.comp_algebraMap]

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ ((↑f).comp (algebraMap R (MvPolynomial ι R))).IsIntegral

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ ((↑f).comp (algebraMap R (MvPolynomial ι R))).IsIntegral

Tactic:
exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ Module.Finite R S

Tactic:
have : (algebraMap R S).IsIntegral := by
  rw [← f.comp_algebraMap]
  #adaptation_note 
  exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing f.toRingHom hf

Result:
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field S
inst✝² : Algebra R S
inst✝¹ : IsJacobsonRing R
inst✝ : Algebra.FiniteType R S
ι : Type u_2
hι : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hf : Function.Surjective ⇑f
this : (algebraMap R S).IsIntegral
⊢ Module.Finite R S