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 : ℕ
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)
have 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)
Tactic: rw [id_comp, Ideal.map_coe]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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)
⊢ 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)
have rw₁ : Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I) (Ideal.map (T f) I)
Tactic: rw [id_comp, Ideal.map_coe]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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 (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)))
have _ : 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: 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]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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 (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)))
have _₁ : 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: 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]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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 (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)))
have _₂ : 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: 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]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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
have 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)
Tactic: have : (T f).symm.toRingEquiv.toRingHom.comp (T f) = RingHom.id _ :=
        RingEquiv.symm_toRingHom_comp_toRingHom _
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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)
⊢ 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
have rw : I =
  Ideal.map (F := MvPolynomial (Fin (n + 1)) k →+* MvPolynomial (Fin (n + 1)) k)
    (RingHom.id (MvPolynomial (Fin (n + 1)) k)) I
Tactic: rw [this, Ideal.map_id]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ 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
have rw₁ : I = I
Tactic: rw [this, Ideal.map_id]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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 (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))
have 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))
Tactic: rw [← Ideal.map_map, Ideal.map_coe, Ideal.map_coe]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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 (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)
have _ : 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: 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
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ 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)
have _₁ : 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: 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
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
have 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
Tactic: refine ⟨0, le_rfl, Quotient.mkₐ k I, fun a b hab ↦ ?_,
      isIntegral_of_surjective _ (Quotient.mkₐ_surjective k I)⟩
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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
have hab₁ : a - b ∈ I
Tactic: rw [Quotient.mkₐ_eq_mk, Ideal.Quotient.eq] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ a = b
have zero : ∀ (ne : ¬a = b), False
Tactic: by_contra ne
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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
⊢ False
have eq : a - b = (MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) (MvPolynomial.coeff 0 (a - b))
Tactic: have eq := eq_C_of_isEmpty (a - b)
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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))
⊢ False
have ne₁ : 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 _
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ False
have zero : ∀ (c : k), MvPolynomial.coeff 0 (a - b) * c = 1 → ∀ (eqr : c * MvPolynomial.coeff 0 (a - b) = 1), False
Tactic: obtain ⟨c, _, eqr⟩ := isUnit_iff_exists.mp ne.isUnit
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
have rw : HMul.hMul (α := MvPolynomial (Fin 0) k) ((MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) c : MvPolynomial (Fin 0) k)
    (a - b) =
  1
Tactic: rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ c • (a - b) = 1
have 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
Tactic: rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ c • (a - b) = 1
have 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)
Tactic: rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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)
⊢ c • (a - b) = 1
have rw₃ : Eq.{u_1 + 1} (α := MvPolynomial (Fin 0) k) ((MvPolynomial.C : (a : k) → MvPolynomial (Fin 0) k) 1) 1
Tactic: rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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
⊢ c • (a - b) = 1
have rw₄ : Eq.{u_1 + 1} (α := MvPolynomial (Fin 0) k) 1 1
Tactic: rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
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
⊢ False
have one : 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]
-- 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 ≠ ⊤
⊢ ∃ 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 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
Tactic: by_cases eqi : I = 0