awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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 ≠ ⊤
pos :
  ∀ (eqi : I = 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
have neg : ∀ (eqi : ¬I = 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
Tactic: by_cases eqi : I = 0
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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
⊢ ∃ 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
have 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)
Tactic: have bij : Function.Bijective (Quotient.mkₐ k I) :=
        (Quotient.mk_bijective_iff_eq_bot I).mpr eqi
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ ∃ 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
have 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
Tactic: obtain ⟨f, fi, fne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot eqi
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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)
⊢ ∃ 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
have this : Nontrivial.{u_1} (MvPolynomial (Fin (d + 1)) k ⧸ I)
Tactic: have := Quotient.nontrivial_iff.mpr hi
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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 ≤ 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
have 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
Tactic: obtain ⟨s, _, g, injg, intg⟩ := hd (ker <| hom2 f I) (ker_ne_top <| hom2 f I)
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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
⊢ ∃ 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
have comp : (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]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin n) k)
hi : I ≠ ⊤
⊢ ∃ 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
have 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
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 _ _⟩
Cleared hypotheses: I, hi
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ ∃ 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
have 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
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 _ _⟩
Cleared hypotheses: I, hi
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨n, f, fsurj⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp fin
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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 : ℕ) (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
have 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
Tactic: obtain ⟨s, _, g, injg, intg⟩ := exists_integral_inj_algHom_of_quotient (ker f) (ker_ne_top _)
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ ∃ (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
have 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
Tactic: use s, ϕ.toAlgHom.comp g
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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.{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
have 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)
Tactic: simp only [AlgHom.coe_comp, AlgEquiv.coe_algHom, EmbeddingLike.comp_injective,
    AlgHom.toRingHom_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ ∃ (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.Finite
have obtain : ∀ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R)
  (inj :
    Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
      (⇑g : (a : MvPolynomial (Fin s) k) → R))
  (int : 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.Finite
Tactic: obtain ⟨s, g, ⟨inj, int⟩⟩ := exists_integral_inj_algHom_of_fg k R
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R) (⇑g : (a : MvPolynomial (Fin s) k) → R)
int : g.IsIntegral
⊢ Eq (α := k →+* R) (algebraMap k R) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
have algebraizeInst : let algInst := g.toAlgebra;
Algebra.IsIntegral.{u_2, u_3} (MvPolynomial (Fin s) k) R
Tactic: algebraize [g.toRingHom]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R) (⇑g : (a : MvPolynomial (Fin s) k) → R)
int : g.IsIntegral
algInst : Algebra.{u_2, u_3} (MvPolynomial (Fin s) k) R := g.toAlgebra
algebraizeInst : Algebra.IsIntegral.{u_2, u_3} (MvPolynomial (Fin s) k) R
⊢ Eq (α := k →+* R) (algebraMap k R) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
have rw : Eq (α := k →+* R)
  (@RingHom.comp _ (MvPolynomial (Fin s) k) _ _ Semiring.toNonAssocSemiring _ (algebraMap (MvPolynomial (Fin s) k) R)
    (algebraMap k (MvPolynomial (Fin s) k)))
  (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
Tactic: rw [IsScalarTower.algebraMap_eq k (MvPolynomial (Fin s) k), algebraMap_toAlgebra']
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R) (⇑g : (a : MvPolynomial (Fin s) k) → R)
int : g.IsIntegral
algInst : Algebra.{u_2, u_3} (MvPolynomial (Fin s) k) R := g.toAlgebra
algebraizeInst : Algebra.IsIntegral.{u_2, u_3} (MvPolynomial (Fin s) k) R
rw :
  Eq (α := k →+* R)
    (@RingHom.comp _ (MvPolynomial (Fin s) k) _ _ Semiring.toNonAssocSemiring _ (algebraMap (MvPolynomial (Fin s) k) R)
      (algebraMap k (MvPolynomial (Fin s) k)))
    (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
⊢ Eq (α := k →+* R) (algebraMap k R) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
have rw₁ : Eq (α := k →+* R) (g.comp (algebraMap k (MvPolynomial (Fin s) k))) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
Tactic: rw [IsScalarTower.algebraMap_eq k (MvPolynomial (Fin s) k), algebraMap_toAlgebra']
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R) (⇑g : (a : MvPolynomial (Fin s) k) → R)
int : 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.Finite
have h : Eq (α := k →+* R) (algebraMap k R) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
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']
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
inst_6 : Finite M
s : Submodule R M
⊢ Submodule.span R (↑(⋯.toFinset (s := (↑s : Set M))) : Set M) = s
have rw : Submodule.span R (↑s : Set M) = s
Tactic: rw [Set.Finite.coe_toFinset, Submodule.span_eq]