awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
set :
  let g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n;
  Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I)
    (Ideal.map (R := (MvPolynomial (Fin n) k)[X]) (F := (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (↑g.symm : (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) g (Ideal.map (T f) I)))
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I)
    (Ideal.map (R := (MvPolynomial (Fin n) k)[X]) (F := (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv k n)) : (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F :=
        MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X]) (MvPolynomial.finSuccEquiv k n)
        (Ideal.map (T f) I)))

Tactic:
set g := (finSuccEquiv k n)

Premises used: MvPolynomial.finSuccEquiv
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
⊢ g.symm.toRingEquiv.toRingHom.comp (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]) =
    RingHom.id (MvPolynomial (Fin (n + 1)) k)

Tactic:
have : g.symm.toRingEquiv.toRingHom.comp g = RingHom.id _ :=
    g.toRingEquiv.symm_toRingHom_comp_toRingHom
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this :
  g.symm.toRingEquiv.toRingHom.comp (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]) =
    RingHom.id (MvPolynomial (Fin (n + 1)) k)
rw :
  Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I)
    (Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k) I)
rw₁ rw₂ : Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I) (Ideal.map (T f) I)
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I)
    (Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (RingHom.comp (RingHom.id (MvPolynomial (Fin (n + 1)) k))
        (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k))
      I)

Tactic:
rw [id_comp, Ideal.map_coe]

Premises used: Ideal.map_coe, RingHom.id_comp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this :
  g.symm.toRingEquiv.toRingHom.comp (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]) =
    RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (RingHom.comp (RingHom.id (MvPolynomial (Fin (n + 1)) k))
        (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k))
      I)
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (RingHom.id (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I))

Tactic:
simp only [← Ideal.map_map, Ideal.map_coe]

Premises used: Ideal.map_map, Ideal.map_coe
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this :
  g.symm.toRingEquiv.toRingHom.comp (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]) =
    RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (RingHom.id (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      ((↑g.symm : (MvPolynomial (Fin n) k)[X] →ₐ[k] MvPolynomial (Fin (n + 1)) k).comp
        (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]))
      (Ideal.map (T f) I))

Tactic:
congrFun (congrArg Ideal.map this.symm) (I.map (T f))

Premises used: congrArg, Ideal.map, MulEquiv.toMonoidHom, congrFun, RingEquiv.toRingHom, Eq.symm, _private.0.NoetherNormalization.T
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this :
  g.symm.toRingEquiv.toRingHom.comp (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]) =
    RingHom.id (MvPolynomial (Fin (n + 1)) k)
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      ((↑g.symm : (MvPolynomial (Fin n) k)[X] →ₐ[k] MvPolynomial (Fin (n + 1)) k).comp
        (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]))
      (Ideal.map (T f) I))
    (Ideal.map (R := (MvPolynomial (Fin n) k)[X]) (F := (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (↑g.symm : (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) g (Ideal.map (T f) I)))

Tactic:
simp [← Ideal.map_map, Ideal.map_coe]

Premises used: Ideal.map_map, Ideal.map_coe
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
this :
  g.symm.toRingEquiv.toRingHom.comp (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]) =
    RingHom.id (MvPolynomial (Fin (n + 1)) k)
_ :
  Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I)
    (Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (RingHom.comp (RingHom.id (MvPolynomial (Fin (n + 1)) k))
        (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k))
      I)
_₁ :
  Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (RingHom.comp (RingHom.id (MvPolynomial (Fin (n + 1)) k))
        (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k))
      I)
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (RingHom.id (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I))
_₂ :
  Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      ((↑g.symm : (MvPolynomial (Fin n) k)[X] →ₐ[k] MvPolynomial (Fin (n + 1)) k).comp
        (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]))
      (Ideal.map (T f) I))
    (Ideal.map (R := (MvPolynomial (Fin n) k)[X]) (F := (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (↑g.symm : (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) g (Ideal.map (T f) I)))
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I)
    (Ideal.map (R := (MvPolynomial (Fin n) k)[X]) (F := (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (↑g.symm : (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) g (Ideal.map (T f) I)))

Tactic:
calc
    _ = Ideal.map ((RingHom.id _).comp <| T f) I := by rw [id_comp, Ideal.map_coe]
    _ = (I.map (T f)).map (RingHom.id _) := by simp only [← Ideal.map_map, Ideal.map_coe]
    _ = (I.map (T f)).map (g.symm.toAlgHom.toRingHom.comp g) :=
      congrFun (congrArg Ideal.map this.symm) (I.map (T f))
    _ = _ := by simp [← Ideal.map_map, Ideal.map_coe]

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, congrArg, Ideal.map, RingHom.comp, AlgHom.toRingHom, congrFun, Eq.symm, RingHom.id, _private.0.NoetherNormalization.T
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ (T f).symm.toRingEquiv.toRingHom.comp (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k) =
    RingHom.id (MvPolynomial (Fin (n + 1)) k)

Tactic:
have : (T f).symm.toRingEquiv.toRingHom.comp (T f) = RingHom.id _ :=
        RingEquiv.symm_toRingHom_comp_toRingHom _
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
this :
  (T f).symm.toRingEquiv.toRingHom.comp (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k) =
    RingHom.id (MvPolynomial (Fin (n + 1)) k)
rw :
  I =
    Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (RingHom.id (MvPolynomial (Fin (n + 1)) k)) I
rw₁ rw₂ : I = I
⊢ I =
    Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      ((T f).symm.toRingEquiv.toRingHom.comp (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)) I

Tactic:
rw [this, Ideal.map_id]

Premises used: Ideal.map_id
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
rw :
  Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (T f).symm.toRingEquiv.toRingHom (Ideal.map (T f) I))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (T f).symm (Ideal.map (T f) I))
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      ((T f).symm.toRingEquiv.toRingHom.comp (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k))
      I)
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (↑(T f).symm : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k) (Ideal.map (T f) I))

Tactic:
rw [← Ideal.map_map, Ideal.map_coe, Ideal.map_coe]

Premises used: Ideal.map_map, Ideal.map_coe
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (T f).symm.toRingEquiv.toRingHom (Ideal.map (T f) I))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (T f).symm (Ideal.map (T f) I))

Tactic:
congrArg _ rfl

Premises used: AlgEquiv.symm, congrArg, Ideal.map, RingEquiv.toRingHom, rfl
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (T f).symm.toRingEquiv.toRingHom (Ideal.map (T f) I))
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (T f).symm (Ideal.map (T f) I))

Tactic:
exact congrArg _ rfl

Premises used: congrArg, rfl
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
_ :
  I =
    Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      ((T f).symm.toRingEquiv.toRingHom.comp (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)) I
_₁ :
  Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k))
    (Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      ((T f).symm.toRingEquiv.toRingHom.comp (↑(T f) : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k))
      I)
    (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (↑(T f).symm : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k) (Ideal.map (T f) I))
⊢ I =
    Ideal.map (R := MvPolynomial (Fin (n + 1)) k) (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
      (↑(T f).symm : MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k) (Ideal.map (T f) I)

Tactic:
calc
    _ = I.map ((T f).symm.toRingEquiv.toRingHom.comp (T f)) := by
      have : (T f).symm.toRingEquiv.toRingHom.comp (T f) = RingHom.id _ :=
        RingEquiv.symm_toRingHom_comp_toRingHom _
      rw [this, Ideal.map_id]
    _ = _ := by
      rw [← Ideal.map_map, Ideal.map_coe, Ideal.map_coe]
      exact congrArg _ rfl

Premises used: AlgEquiv.symm, Ideal.map, RingHom.comp, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, _private.0.NoetherNormalization.T
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
I : Ideal (MvPolynomial (Fin (n + 1)) k)
fne : f ≠ 0
fi : f ∈ I
⊢ (hom2 f I).IsIntegral

Tactic:
((hom1_isIntegral f I fne fi).trans _ _ <| isIntegral_of_surjective _ (eqv1 f I).surjective).trans
    _ _ <| isIntegral_of_surjective _ (eqv2 f I).surjective

Premises used: RingHom.isIntegral_of_surjective, RingHom.IsIntegral.trans, AlgEquiv.surjective, _private.0.NoetherNormalization.eqv2
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
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:
⟨0, le_rfl, Quotient.mkₐ k I, fun a b hab ↦ ?_,
      isIntegral_of_surjective _ (Quotient.mkₐ_surjective k I)⟩

Premises used: le_rfl, RingHom.isIntegral_of_surjective, And.intro, Exists.intro, OfNat.ofNat, Ideal.Quotient.mkₐ, Ideal.Quotient.mkₐ_surjective
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
zero :
  ∀ (a b : MvPolynomial (Fin 0) k)
    (hab :
      Eq (α := MvPolynomial (Fin 0) k ⧸ I)
        ((Quotient.mkₐ k I : (a : MvPolynomial (Fin 0) k) → MvPolynomial (Fin 0) k ⧸ I) a : MvPolynomial (Fin 0) k ⧸ I)
        ((Quotient.mkₐ k I : (a : MvPolynomial (Fin 0) k) → MvPolynomial (Fin 0) k ⧸ I) b :
          MvPolynomial (Fin 0) k ⧸ I)),
    a = b
⊢ ∃ 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:
refine ⟨0, le_rfl, Quotient.mkₐ k I, fun a b hab ↦ ?_,
      isIntegral_of_surjective _ (Quotient.mkₐ_surjective k I)⟩
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab :
  Eq (α := MvPolynomial (Fin 0) k ⧸ I)
    ((Quotient.mkₐ k I : (a : MvPolynomial (Fin 0) k) → MvPolynomial (Fin 0) k ⧸ I) a : MvPolynomial (Fin 0) k ⧸ I)
    ((Quotient.mkₐ k I : (a : MvPolynomial (Fin 0) k) → MvPolynomial (Fin 0) k ⧸ I) b : MvPolynomial (Fin 0) k ⧸ I)
⊢ a - b ∈ I

Tactic:
rw [Quotient.mkₐ_eq_mk, Ideal.Quotient.eq] at hab

Premises used: Ideal.Quotient.eq, Ideal.Quotient.mkₐ_eq_mk
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
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
zero : ∀ (ne : ¬a = b), False
⊢ a = b

Tactic:
by_contra ne
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
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
ne : ¬a = b
⊢ a - b = (MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (MvPolynomial.coeff 0 (a - b))

Tactic:
have eq := eq_C_of_isEmpty (a - b)
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
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
ne : ¬a = b
eq : a - b = (MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (MvPolynomial.coeff 0 (a - b))
⊢ MvPolynomial.coeff 0 (a - b) ≠ 0

Tactic:
have ne : coeff 0 (a - b) ≠ 0 := fun h ↦ h ▸ eq ▸ sub_ne_zero_of_ne ne <| map_zero _
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
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
ne_1 : ¬a = b
eq : a - b = (MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
zero : ∀ (c : k), MvPolynomial.coeff 0 (a - b) * c = 1 → ∀ (eqr : c * MvPolynomial.coeff 0 (a - b) = 1), False
⊢ False

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

Premises used: isUnit_iff_exists, Ne.isUnit, Iff.mp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
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
ne_1 : ¬a = b
eq : a - b = (MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (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
rw :
  HMul.hMul (α := MvPolynomial (Fin 0) k)
      ((MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) c : MvPolynomial (Fin 0) k) (a - b) =
    1
rw₁ :
  HMul.hMul (α := MvPolynomial (Fin 0) k) (β := MvPolynomial (Fin 0) k)
      ((MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) c : MvPolynomial (Fin 0) k)
      ((MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (MvPolynomial.coeff 0 (a - b)) : MvPolynomial (Fin 0) k) =
    1
rw₂ :
  Eq (α := MvPolynomial (Fin 0) k)
    ((MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (c * MvPolynomial.coeff 0 (a - b)) : MvPolynomial (Fin 0) k)
    (1 : MvPolynomial (Fin 0) k)
rw₃ : Eq.{u_1 + 1} (α := MvPolynomial (Fin 0) k) ((MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) 1) 1
rw₄ rw₅ : Eq.{u_1 + 1} (α := MvPolynomial (Fin 0) k) 1 1
⊢ c • (a - b) = 1

Tactic:
rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]

Premises used: MvPolynomial.C_1, map_mul, MvPolynomial.smul_eq_C_mul
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
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
ne_1 : ¬a = b
eq : a - b = (MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (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
⊢ c • (a - b) = 1

Tactic:
have one : c • (a - b) = 1 := by
      rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
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
ne_1 : ¬a = b
eq : a - b = (MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (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
one : c • (a - b) = 1
⊢ False

Tactic:
hi ((eq_top_iff_one I).mpr (one ▸ I.smul_of_tower_mem c hab))

Premises used: Iff.mpr, Eq.rec, Ideal.eq_top_iff_one, Submodule.smul_of_tower_mem
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
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
ne_1 : ¬a = b
eq : a - b = (MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (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
one : c • (a - b) = 1
⊢ False

Tactic:
exact hi ((eq_top_iff_one I).mpr (one ▸ I.smul_of_tower_mem c hab))

Premises used: Iff.mpr, Eq.rec, Ideal.eq_top_iff_one, Submodule.smul_of_tower_mem
-- 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 ≠ ⊤
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
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
⊢ ∃ 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
-- 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
⊢ 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