-- Mathlib/RingTheory/NoetherNormalization.lean
theorem exists_integral_inj_algHom_of_quotient (I : Ideal (MvPolynomial (Fin n) k))
    (hi : I ≠ ⊤) : ∃ s ≤ n, ∃ g : (MvPolynomial (Fin s) k) →ₐ[k] ((MvPolynomial (Fin n) k) ⧸ I),
    Function.Injective g ∧ g.IsIntegral

Proof state:
case neg.intro.intro
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
set ϕ := kerLiftAlg <| hom2 f I

Result:
case neg.intro.intro
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (NoetherNormalization.hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (NoetherNormalization.hom2 f I)
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Proof state:
case zero
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
neq : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
⊢ False

Tactic:
obtain ⟨c, _, eqr⟩ := isUnit_iff_exists.mp ne.isUnit

Result:
case zero.intro.intro
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
neq : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
c : k
left✝ : MvPolynomial.coeff 0 (a - b) * c = 1
eqr : c * MvPolynomial.coeff 0 (a - b) = 1
⊢ False

Proof state:
case neg.intro.intro.intro.intro.intro.intro
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (NoetherNormalization.hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (NoetherNormalization.hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left✝ : s ≤ d
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ ker (NoetherNormalization.hom2 f I)
injg : Function.Injective ⇑g
intg : g.IsIntegral
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
have comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k <| ker <| hom2 f I) = (hom2 f I) :=
  AlgHom.ext fun a ↦ by
    simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk]

Result:
case neg.intro.intro.intro.intro.intro.intro
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (NoetherNormalization.hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (NoetherNormalization.hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left✝ : s ≤ d
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ ker (NoetherNormalization.hom2 f I)
injg : Function.Injective ⇑g
intg : g.IsIntegral
comp :
  (kerLiftAlg (NoetherNormalization.hom2 f I)).comp (Quotient.mkₐ k (ker (NoetherNormalization.hom2 f I))) =
    NoetherNormalization.hom2 f I
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Proof state:
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (NoetherNormalization.hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (NoetherNormalization.hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left✝ : s ≤ d
g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ ker (NoetherNormalization.hom2 f I)
injg : Function.Injective ⇑g
intg : g.IsIntegral
a : MvPolynomial (Fin d) k
⊢ ((kerLiftAlg (NoetherNormalization.hom2 f I)).comp (Quotient.mkₐ k (ker (NoetherNormalization.hom2 f I)))) a =
    (NoetherNormalization.hom2 f I) a

Tactic:
simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk]

Result:
no goals

Proof state:
case neg
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
obtain ⟨f, fi, fne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot eqi

Result:
case neg.intro.intro
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Proof state:
case succ
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
by_cases eqi : I = 0

Result:
case pos
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : I = 0
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

case neg
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Proof state:
case zero
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
⊢ ∃ s ≤ 0, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
refine ⟨0, le_rfl, Quotient.mkₐ k I, fun a b hab ↦ ?_,
  isIntegral_of_surjective _ (Quotient.mkₐ_surjective k I)⟩

Result:
case zero
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : (Quotient.mkₐ k I) a = (Quotient.mkₐ k I) b
⊢ a = b

Proof state:
case neg.intro.intro
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (NoetherNormalization.hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (NoetherNormalization.hom2 f I)
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
have := Quotient.nontrivial hi

Result:
case neg.intro.intro
k : Type u_1
inst✝ : Field k
n d : ℕ
hd : ∀ (I : Ideal (MvPolynomial (Fin d) k)), I ≠ ⊤ → ∃ s ≤ d, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
f : MvPolynomial (Fin (d + 1)) k
fi : f ∈ I
fne : f ≠ 0
ϕ : MvPolynomial (Fin d) k ⧸ ker (NoetherNormalization.hom2 f I) →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (NoetherNormalization.hom2 f I)
this : Nontrivial (MvPolynomial (Fin (d + 1)) k ⧸ I)
⊢ ∃ s ≤ d + 1, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral