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

Proof state:
case intro.intro.intro.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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left✝ : s ≤ n
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin n) k ⧸ ker f
injg : Function.Injective ⇑g
intg : g.IsIntegral
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
use s, ϕ.toAlgHom.comp g

Result:
case h
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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left✝ : s ≤ n
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin n) k ⧸ ker f
injg : Function.Injective ⇑g
intg : g.IsIntegral
⊢ Function.Injective ⇑((↑ϕ).comp g) ∧ ((↑ϕ).comp g).IsIntegral

Proof state:
case 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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
set ϕ := quotientKerAlgEquivOfSurjective fsurj

Result:
case 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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral

Proof state:
case 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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
obtain ⟨s, _, g, injg, intg⟩ := exists_integral_inj_algHom_of_quotient (ker f) (ker_ne_top _)

Result:
case intro.intro.intro.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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left✝ : s ≤ n
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin n) k ⧸ ker f
injg : Function.Injective ⇑g
intg : g.IsIntegral
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral

Proof state:
case h
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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left✝ : s ≤ n
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin n) k ⧸ ker f
injg : Function.Injective ⇑g
intg : g.IsIntegral
⊢ Function.Injective ⇑g ∧ (↑((↑ϕ).comp g)).IsIntegral

Tactic:
exact ⟨injg, intg.trans _ _ (isIntegral_of_surjective _ ϕ.surjective)⟩

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, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
obtain ⟨n, f, fsurj⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp fin

Result:
case 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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
⊢ ∃ s g, Function.Injective ⇑g ∧ g.IsIntegral

Proof state:
case h
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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left✝ : s ≤ n
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin n) k ⧸ ker f
injg : Function.Injective ⇑g
intg : g.IsIntegral
⊢ Function.Injective ⇑((↑ϕ).comp g) ∧ ((↑ϕ).comp g).IsIntegral

Tactic:
simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe,
  EmbeddingLike.comp_injective, AlgHom.toRingHom_eq_coe]

Result:
case h
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
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj : Function.Surjective ⇑f
ϕ : (MvPolynomial (Fin n) k ⧸ ker f) ≃ₐ[k] R := quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left✝ : s ≤ n
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin n) k ⧸ ker f
injg : Function.Injective ⇑g
intg : g.IsIntegral
⊢ Function.Injective ⇑g ∧ (↑((↑ϕ).comp g)).IsIntegral