awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n d : ℕ
hd :
  ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
          g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : I = 0
bij :
  Function.Bijective (α := MvPolynomial (Fin (d + 1)) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
    (⇑(Quotient.mkₐ k I) : (a : MvPolynomial (Fin (d + 1)) k) → MvPolynomial (Fin (d + 1)) k ⧸ I)
⊢ ∃ s ≤ d + 1,
    ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I),
      Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
          (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin (d + 1)) k ⧸ I) ∧
        g.IsIntegral

Tactic:
⟨d + 1, le_rfl, _, bij.1, isIntegral_of_surjective _ bij.2⟩

Premises used: le_rfl, RingHom.isIntegral_of_surjective, And.right, And.left, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n d : ℕ
hd :
  ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
          g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : I = 0
bij :
  Function.Bijective (α := MvPolynomial (Fin (d + 1)) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
    (⇑(Quotient.mkₐ k I) : (a : MvPolynomial (Fin (d + 1)) k) → MvPolynomial (Fin (d + 1)) k ⧸ I)
⊢ ∃ s ≤ d + 1,
    ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I),
      Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
          (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin (d + 1)) k ⧸ I) ∧
        g.IsIntegral

Tactic:
exact ⟨d + 1, le_rfl, _, bij.1, isIntegral_of_surjective _ bij.2⟩
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n d : ℕ
hd :
  ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
          g.IsIntegral
I : Ideal (MvPolynomial (Fin (d + 1)) k)
hi : I ≠ ⊤
eqi : ¬I = 0
neg :
  ∀ (f : MvPolynomial (Fin (d + 1)) k) (fi : f ∈ I) (fne : f ≠ 0),
    ∃ s ≤ d + 1,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin (d + 1)) k ⧸ I) ∧
          g.IsIntegral
⊢ ∃ s ≤ d + 1,
    ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I),
      Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
          (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin (d + 1)) k ⧸ I) ∧
        g.IsIntegral

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

Premises used: Submodule.exists_mem_ne_zero_of_ne_bot
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n d : ℕ
hd :
  ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
          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
ϕ : HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)) →ₐ[k]
  MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (hom2 f I)
⊢ Nontrivial.{u_1} (MvPolynomial (Fin (d + 1)) k ⧸ I)

Tactic:
have := Quotient.nontrivial_iff.mpr hi
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n d : ℕ
hd :
  ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
          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
ϕ : HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)) →ₐ[k]
  MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (hom2 f I)
this : Nontrivial.{u_1} (MvPolynomial (Fin (d + 1)) k ⧸ I)
neg :
  ∀ s ≤ d,
    ∀
      (g :
        MvPolynomial (Fin s) k →ₐ[k]
          HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)))
      (injg :
        Function.Injective (α := MvPolynomial (Fin s) k) (β :=
          HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)))
          (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ ker (hom2 f I)))
      (intg : g.IsIntegral),
      ∃ s ≤ d + 1,
        ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I),
          Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
              (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin (d + 1)) k ⧸ I) ∧
            g.IsIntegral
⊢ ∃ s ≤ d + 1,
    ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I),
      Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
          (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin (d + 1)) k ⧸ I) ∧
        g.IsIntegral

Tactic:
obtain ⟨s, _, g, injg, intg⟩ := hd (ker <| hom2 f I) (ker_ne_top <| hom2 f I)

Premises used: RingHom.ker_ne_top, _private.0.NoetherNormalization.hom2, RingHom.ker
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n d : ℕ
hd :
  ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
          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
ϕ : HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)) →ₐ[k]
  MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (hom2 f I)
this : Nontrivial.{u_1} (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left : s ≤ d
g :
  MvPolynomial (Fin s) k →ₐ[k]
    HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I))
injg :
  Function.Injective (α := MvPolynomial (Fin s) k) (β :=
    HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)))
    (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ ker (hom2 f I))
intg : g.IsIntegral
a : MvPolynomial (Fin d) k
⊢ Eq (α := MvPolynomial (Fin (d + 1)) k ⧸ I)
    (((kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k (ker (hom2 f I))) :
          (a : MvPolynomial (Fin d) k) → MvPolynomial (Fin (d + 1)) k ⧸ I)
        a :
      MvPolynomial (Fin (d + 1)) k ⧸ I)
    ((hom2 f I : (a : MvPolynomial (Fin d) k) → MvPolynomial (Fin (d + 1)) k ⧸ I) a : MvPolynomial (Fin (d + 1)) k ⧸ I)

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

Premises used: AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply, Ideal.kerLiftAlg_mk
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n d : ℕ
hd :
  ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
          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
ϕ : HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)) →ₐ[k]
  MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (hom2 f I)
this : Nontrivial.{u_1} (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left : s ≤ d
g :
  MvPolynomial (Fin s) k →ₐ[k]
    HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I))
injg :
  Function.Injective (α := MvPolynomial (Fin s) k) (β :=
    HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)))
    (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ ker (hom2 f I))
intg : g.IsIntegral
⊢ (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k (ker (hom2 f I))) = hom2 f I

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]
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n d : ℕ
hd :
  ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
          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
ϕ : HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)) →ₐ[k]
  MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (hom2 f I)
this : Nontrivial.{u_1} (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left : s ≤ d
g :
  MvPolynomial (Fin s) k →ₐ[k]
    HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I))
injg :
  Function.Injective (α := MvPolynomial (Fin s) k) (β :=
    HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)))
    (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ ker (hom2 f I))
intg : g.IsIntegral
comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k (ker (hom2 f I))) = hom2 f I
⊢ s ≤ d + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n d : ℕ
hd :
  ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
          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
ϕ : HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)) →ₐ[k]
  MvPolynomial (Fin (d + 1)) k ⧸ I :=
  kerLiftAlg (hom2 f I)
this : Nontrivial.{u_1} (MvPolynomial (Fin (d + 1)) k ⧸ I)
s : ℕ
left : s ≤ d
g :
  MvPolynomial (Fin s) k →ₐ[k]
    HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I))
injg :
  Function.Injective (α := MvPolynomial (Fin s) k) (β :=
    HasQuotient.Quotient (MvPolynomial (Fin d) k) (B := Ideal (MvPolynomial (Fin d) k)) (ker (hom2 f I)))
    (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ ker (hom2 f I))
intg : g.IsIntegral
comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k (ker (hom2 f I))) = hom2 f I
⊢ ∃ s ≤ d + 1,
    ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I),
      Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
          (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin (d + 1)) k ⧸ I) ∧
        g.IsIntegral

Tactic:
exact ⟨s, by lia, ϕ.comp g, (ϕ.coe_comp  g) ▸ (kerLiftAlg_injective _).comp injg,
        intg.trans _ _ <| (comp ▸ hom2_isIntegral f I fne fi).tower_top _ _⟩
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin n) k)
hi : I ≠ ⊤
zero :
  ∀ (I : Ideal (MvPolynomial (Fin 0) k)) (hi : I ≠ ⊤),
    ∃ s ≤ 0,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin 0) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin 0) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin 0) k ⧸ I) ∧
          g.IsIntegral
succ :
  ∀ (d : ℕ)
    (hd :
      ∀ (I : Ideal (MvPolynomial (Fin d) k)) (hi : I ≠ ⊤),
        ∃ s ≤ d,
          ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin d) k ⧸ I),
            Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin d) k ⧸ I)
                (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin d) k ⧸ I) ∧
              g.IsIntegral)
    (I : Ideal (MvPolynomial (Fin (d + 1)) k)) (hi : I ≠ ⊤),
    ∃ s ≤ d + 1,
      ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin (d + 1)) k ⧸ I),
        Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin (d + 1)) k ⧸ I)
            (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin (d + 1)) k ⧸ I) ∧
          g.IsIntegral
⊢ ∃ s ≤ n,
    ∃ (g : MvPolynomial (Fin s) k →ₐ[k] MvPolynomial (Fin n) k ⧸ I),
      Function.Injective (α := MvPolynomial (Fin s) k) (β := MvPolynomial (Fin n) k ⧸ I)
          (⇑g : (a : MvPolynomial (Fin s) k) → MvPolynomial (Fin n) k ⧸ I) ∧
        g.IsIntegral

Tactic:
induction n with
  | zero =>
    refine ⟨0, le_rfl, Quotient.mkₐ k I, fun a b hab ↦ ?_,
      isIntegral_of_surjective _ (Quotient.mkₐ_surjective k I)⟩
    rw [Quotient.mkₐ_eq_mk, Ideal.Quotient.eq] at hab
    by_contra ne
    have eq := eq_C_of_isEmpty (a - b)
    have ne : coeff 0 (a - b) ≠ 0 := fun h ↦ h ▸ eq ▸ sub_ne_zero_of_ne ne <| map_zero _
    obtain ⟨c, _, eqr⟩ := isUnit_iff_exists.mp ne.isUnit
    have one : c • (a - b) = 1 := by
      rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]
    exact hi ((eq_top_iff_one I).mpr (one ▸ I.smul_of_tower_mem c hab))
  | succ d hd =>
    by_cases eqi : I = 0
    · have bij : Function.Bijective (Quotient.mkₐ k I) :=
        (Quotient.mk_bijective_iff_eq_bot I).mpr eqi
      exact ⟨d + 1, le_rfl, _, bij.1, isIntegral_of_surjective _ bij.2⟩
    · obtain ⟨f, fi, fne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot eqi
      set ϕ := kerLiftAlg <| hom2 f I
      have := Quotient.nontrivial_iff.mpr hi
      obtain ⟨s, _, g, injg, intg⟩ := hd (ker <| hom2 f I) (ker_ne_top <| hom2 f I)
      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]
      exact ⟨s, by lia, ϕ.comp g, (ϕ.coe_comp  g) ▸ (kerLiftAlg_injective _).comp injg,
        intg.trans _ _ <| (comp ▸ hom2_isIntegral f I fne fi).tower_top _ _⟩

Premises used: Ideal.Quotient.eq, Ideal.Quotient.mkₐ_eq_mk, Nat.zero, Nat.succ, Ideal.kerLiftAlg
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
obtain :
  ∀ (n : ℕ) (f : MvPolynomial (Fin n) k →ₐ[k] R)
    (fsurj :
      Function.Surjective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin n) k) (β := R)
        (⇑f : (a : MvPolynomial (Fin n) k) → R)),
    ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R),
      Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
          (⇑g : (a : MvPolynomial (Fin s) k) → R) ∧
        g.IsIntegral
⊢ ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R),
    Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
        (⇑g : (a : MvPolynomial (Fin s) k) → R) ∧
      g.IsIntegral

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

Premises used: Iff.mp, Algebra.FiniteType.iff_quotient_mvPolynomial''
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin n) k) (β := R) (⇑f : (a : MvPolynomial (Fin n) k) → R)
ϕ : HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f) ≃ₐ[k] R :=
  quotientKerAlgEquivOfSurjective fsurj
obtain :
  ∀ s ≤ n,
    ∀
      (g :
        MvPolynomial (Fin s) k →ₐ[k]
          HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f))
      (injg :
        Function.Injective (α := MvPolynomial (Fin s) k) (β :=
          HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f))
          (⇑g : (a_1 : MvPolynomial (Fin s) k) → MvPolynomial (Fin n) k ⧸ ker f))
      (intg : g.IsIntegral),
      ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R),
        Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
            (⇑g : (a : MvPolynomial (Fin s) k) → R) ∧
          g.IsIntegral
⊢ ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R),
    Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
        (⇑g : (a : MvPolynomial (Fin s) k) → R) ∧
      g.IsIntegral

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

Premises used: exists_integral_inj_algHom_of_quotient, RingHom.ker_ne_top, RingHom.ker
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin n) k) (β := R) (⇑f : (a : MvPolynomial (Fin n) k) → R)
ϕ : HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f) ≃ₐ[k] R :=
  quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left : s ≤ n
g :
  MvPolynomial (Fin s) k →ₐ[k]
    HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f)
injg :
  Function.Injective (α := MvPolynomial (Fin s) k) (β :=
    HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f))
    (⇑g : (a_1 : MvPolynomial (Fin s) k) → MvPolynomial (Fin n) k ⧸ ker f)
intg : g.IsIntegral
h :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
      (⇑((↑ϕ : MvPolynomial (Fin n) k ⧸ ker f →ₐ[k] R).comp g) : (a : MvPolynomial (Fin s) k) → R) ∧
    ((↑ϕ : MvPolynomial (Fin n) k ⧸ ker f →ₐ[k] R).comp g).IsIntegral
⊢ ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R),
    Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
        (⇑g : (a : MvPolynomial (Fin s) k) → R) ∧
      g.IsIntegral

Tactic:
use s, ϕ.toAlgHom.comp g

Premises used: AlgEquiv.toAlgHom, AlgHom.comp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin n) k) (β := R) (⇑f : (a : MvPolynomial (Fin n) k) → R)
ϕ : HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f) ≃ₐ[k] R :=
  quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left : s ≤ n
g :
  MvPolynomial (Fin s) k →ₐ[k]
    HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f)
injg :
  Function.Injective (α := MvPolynomial (Fin s) k) (β :=
    HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f))
    (⇑g : (a_1 : MvPolynomial (Fin s) k) → MvPolynomial (Fin n) k ⧸ ker f)
intg : g.IsIntegral
h :
  Function.Injective (α := MvPolynomial (Fin s) k) (β :=
      HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f))
      (⇑g : (a_1 : MvPolynomial (Fin s) k) → MvPolynomial (Fin n) k ⧸ ker f) ∧
    RingHom.IsIntegral (↑((↑ϕ : MvPolynomial (Fin n) k ⧸ ker f →ₐ[k] R).comp g) : MvPolynomial (Fin s) k →+* R)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
      (⇑((↑ϕ : MvPolynomial (Fin n) k ⧸ ker f →ₐ[k] R).comp g) : (a : MvPolynomial (Fin s) k) → R) ∧
    ((↑ϕ : MvPolynomial (Fin n) k ⧸ ker f →ₐ[k] R).comp g).IsIntegral

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

Premises used: EmbeddingLike.comp_injective, AlgHom.coe_comp, AlgEquiv.coe_algHom, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin n) k) (β := R) (⇑f : (a : MvPolynomial (Fin n) k) → R)
ϕ : HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f) ≃ₐ[k] R :=
  quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left : s ≤ n
g :
  MvPolynomial (Fin s) k →ₐ[k]
    HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f)
injg :
  Function.Injective (α := MvPolynomial (Fin s) k) (β :=
    HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f))
    (⇑g : (a_1 : MvPolynomial (Fin s) k) → MvPolynomial (Fin n) k ⧸ ker f)
intg : g.IsIntegral
⊢ Function.Injective (α := MvPolynomial (Fin s) k) (β :=
      HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f))
      (⇑g : (a_1 : MvPolynomial (Fin s) k) → MvPolynomial (Fin n) k ⧸ ker f) ∧
    RingHom.IsIntegral (↑((↑ϕ : MvPolynomial (Fin n) k ⧸ ker f →ₐ[k] R).comp g) : MvPolynomial (Fin s) k →+* R)

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

Premises used: RingHom.isIntegral_of_surjective, RingHom.IsIntegral.trans, And.intro, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
n : ℕ
f : MvPolynomial (Fin n) k →ₐ[k] R
fsurj :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin n) k) (β := R) (⇑f : (a : MvPolynomial (Fin n) k) → R)
ϕ : HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f) ≃ₐ[k] R :=
  quotientKerAlgEquivOfSurjective fsurj
s : ℕ
left : s ≤ n
g :
  MvPolynomial (Fin s) k →ₐ[k]
    HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f)
injg :
  Function.Injective (α := MvPolynomial (Fin s) k) (β :=
    HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f))
    (⇑g : (a_1 : MvPolynomial (Fin s) k) → MvPolynomial (Fin n) k ⧸ ker f)
intg : g.IsIntegral
⊢ Function.Injective (α := MvPolynomial (Fin s) k) (β :=
      HasQuotient.Quotient (MvPolynomial (Fin n) k) (B := Ideal (MvPolynomial (Fin n) k)) (ker f))
      (⇑g : (a_1 : MvPolynomial (Fin s) k) → MvPolynomial (Fin n) k ⧸ ker f) ∧
    RingHom.IsIntegral (↑((↑ϕ : MvPolynomial (Fin n) k ⧸ ker f →ₐ[k] R).comp g) : MvPolynomial (Fin s) k →+* R)

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