-- Mathlib/RingTheory/NoetherNormalization.lean
theorem exists_finite_inj_algHom_of_fg : ∃ s, ∃ g : (MvPolynomial (Fin s) k) →ₐ[k] R,
    Function.Injective g ∧ g.Finite

Proof state:
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
algInst✝ : Algebra (MvPolynomial (Fin s) k) R := g.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral (MvPolynomial (Fin s) k) R
⊢ algebraMap k R = g.comp (algebraMap k (MvPolynomial (Fin s) k))

Tactic:
rw [IsScalarTower.algebraMap_eq k (MvPolynomial (Fin s) k), algebraMap_toAlgebra']

Result:
no goals

Proof state:
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
⊢ algebraMap k R = g.comp (algebraMap k (MvPolynomial (Fin s) k))

Tactic:
algebraize [g.toRingHom]

Result:
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
algInst✝ : Algebra (MvPolynomial (Fin s) k) R := g.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral (MvPolynomial (Fin s) k) R
⊢ algebraMap k R = g.comp (algebraMap k (MvPolynomial (Fin s) k))

Proof state:
case intro.intro.intro
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
h : algebraMap k R = g.comp (algebraMap k (MvPolynomial (Fin s) k))
⊢ ∃ s g, Function.Injective ⇑g ∧ g.Finite

Tactic:
exact ⟨s, g, inj, int.to_finite
  (h ▸ algebraMap_finiteType_iff_algebra_finiteType.mpr fin).of_comp_finiteType⟩

Result:
no goals

Proof state:
case intro.intro.intro
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
⊢ ∃ s g, Function.Injective ⇑g ∧ g.Finite

Tactic:
have h : algebraMap k R = g.toRingHom.comp (algebraMap k (MvPolynomial (Fin s) k)) := by
  algebraize [g.toRingHom]
  rw [IsScalarTower.algebraMap_eq k (MvPolynomial (Fin s) k), algebraMap_toAlgebra']

Result:
case intro.intro.intro
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
h : algebraMap k R = g.comp (algebraMap k (MvPolynomial (Fin s) k))
⊢ ∃ s g, Function.Injective ⇑g ∧ g.Finite

Proof state:
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
⊢ ∃ s g, Function.Injective ⇑g ∧ g.Finite

Tactic:
obtain ⟨s, g, ⟨inj, int⟩⟩ := exists_integral_inj_algHom_of_fg k R

Result:
case intro.intro.intro
k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
⊢ ∃ s g, Function.Injective ⇑g ∧ g.Finite