awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
h₁ :
  ∀ (x : M) (hx : x ∈ p),
    Eq.{u_3 + 1} (α := M)
      (↑((LinearMap.restrict f hp ^ n : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)
      (↑((0 : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)
⊢ LinearMap.restrict f hp ^ n = 0

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
x : M
hx : x ∈ p
⊢ Eq (α := ↥q) ((LinearMap.restrict f hq ^ n : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : ↥q)
    ((0 : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : ↥q)

Tactic:
replace hn := DFunLike.congr_fun hn ⟨x, h hx⟩
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn :
  Eq (α := ↥q) ((LinearMap.restrict f hq ^ n : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : ↥q)
    ((0 : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : ↥q)
h₁ :
  Eq (α := ↥p) ((LinearMap.restrict f hp ^ n : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : ↥p)
    (0 : ↥p)
⊢ Eq.{u_3 + 1} (α := M)
    (↑((LinearMap.restrict f hp ^ n : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)
    (↑((0 : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx)) : M)

Tactic:
simp_rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero] at hn ⊢

Premises used: ZeroMemClass.coe_eq_zero, LinearMap.zero_apply, ZeroMemClass.coe_zero
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn :
  Eq (α := ↥q) ((LinearMap.restrict f hq ^ n : (a : ↥q) → ↥q) (Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : ↥q) (0 : ↥q)
h₁ :
  ∀
    (hn :
      Eq (α := ↥q)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ q)
            ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : M)) ⋯ :
          ↥q)
        (0 : ↥q)),
    Eq (α := ↥p)
      (Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M))
          ⋯ :
        ↥p)
      (0 : ↥p)
⊢ Eq (α := ↥p) ((LinearMap.restrict f hp ^ n : (a : ↥p) → ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : ↥p)
    (0 : ↥p)

Tactic:
rw [Module.End.pow_restrict, LinearMap.restrict_apply] at hn ⊢

Premises used: Module.End.pow_apply_mem_of_forall_mem, Module.End.pow_restrict, LinearMap.restrict_apply
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn :
  Eq (α := ↥q)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ q) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : M))
        ⋯ :
      ↥q)
    (0 : ↥q)
h₁ :
  Eq (α := M)
    ((↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p)
            ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M)) ⋯) :
        M) :
      M)
    ((↑0 : M) : M)
⊢ Eq (α := ↥p)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M))
        ⋯ :
      ↥p)
    (0 : ↥p)

Tactic:
ext
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn :
  Eq (α := ↥q)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ q) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : M))
        ⋯ :
      ↥q)
    (0 : ↥q)
⊢ Eq (α := M)
    ((↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p)
            ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M)) ⋯) :
        M) :
      M)
    ((↑0 : M) : M)

Tactic:
(congr_arg Subtype.val hn :)

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hq : MapsTo (⇑f : (a : M) → M) (↑q : Set M) (↑q : Set M)
h : p ≤ q
n : ℕ
x : M
hx : x ∈ p
hn :
  Eq (α := ↥q)
    (Subtype.mk (p := fun (x : M) ↦ x ∈ q) ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ q) x ⋯) : M))
        ⋯ :
      ↥q)
    (0 : ↥q)
⊢ Eq (α := M)
    ((↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p)
            ((f ^ n : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M)) ⋯) :
        M) :
      M)
    ((↑0 : M) : M)

Tactic:
exact (congr_arg Subtype.val hn :)

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hnil : IsNilpotent f
obtain : ∀ (n : ℕ) (hn : f ^ n = 0), IsNilpotent (f.restrict hf)
⊢ IsNilpotent (f.restrict hf)

Tactic:
obtain ⟨n, hn⟩ := hnil
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
n : ℕ
hn : f ^ n = 0
m : ↥p
simp : Eq (α := ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) 0 ⋯ : ↥p) (0 : ↥p)
⊢ Eq (α := ↥p) ((f.restrict hf ^ n : (a : ↥p) → ↥p) m : ↥p) ((0 : (a : ↥p) → ↥p) m : ↥p)

Tactic:
simp only [Module.End.pow_restrict n, hn,
    LinearMap.restrict_apply, LinearMap.zero_apply]

Premises used: Module.End.pow_apply_mem_of_forall_mem, LinearMap.zero_apply, Module.End.pow_restrict, LinearMap.restrict_apply
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
n : ℕ
hn : f ^ n = 0
m : ↥p
⊢ Eq (α := ↥p) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) 0 ⋯ : ↥p) (0 : ↥p)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : M →ₗ[R] M
p : Submodule R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent (f.restrict hf)

Tactic:
exact ⟨n, LinearMap.ext fun m ↦ by simp only [Module.End.pow_restrict n, hn,
    LinearMap.restrict_apply, LinearMap.zero_apply]; rfl⟩
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
hnp : IsNilpotent f
obtain : ∀ (k : ℕ) (hk : f ^ k = 0), IsNilpotent (p.mapQ p f hp)
⊢ IsNilpotent (p.mapQ p f hp)

Tactic:
obtain ⟨k, hk⟩ := hnp
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
h : p.mapQ p f hp ^ k = 0
⊢ IsNilpotent (p.mapQ p f hp)

Tactic:
use k
-- Module: Mathlib.RingTheory.Nilpotent.Lemmas
Goal:
R : Type u_1
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ p.mapQ p f hp ^ k = 0

Tactic:
simp [← p.mapQ_pow, hk]

Premises used: Submodule.mapQ_pow, Submodule.le_comap_pow_of_le_comap
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), (v : (a : Fin (n + 1)) → ℕ) i < up
⊢ ∀ (l : ℕ), Membership.mem (γ := List ℕ) (ofFn (n := n + 1) (⇑v : (a : Fin (n + 1)) → ℕ)) l → l < up

Tactic:
grind
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
rw :
  Eq.{u_1 + 1} (α := MvPolynomial (Fin (n + 1)) k →ₐ[k] MvPolynomial (Fin (n + 1)) k)
    (MvPolynomial.aeval fun (i : Fin (n + 1)) ↦
      (T1 f c : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (if i = 0 then MvPolynomial.X 0
        else MvPolynomial.X i + -c • HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X 0) (r i)))
    (MvPolynomial.aeval MvPolynomial.X)
⊢ (T1 f c).comp (T1 f (-c)) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Tactic:
rw [comp_aeval, ← MvPolynomial.aeval_X_left]

Premises used: MvPolynomial.aeval_X_left, MvPolynomial.comp_aeval
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
hf :
  ∀ (i : Fin (n + 1)) (v : Fin (n + 1) →₀ ℕ),
    Eq.{u_1 + 1} (α := k)
      (MvPolynomial.coeff v
        ((MvPolynomial.aeval fun (i : Fin (n + 1)) ↦
              (T1 f c : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
                (if i = 0 then MvPolynomial.X 0
                else
                  MvPolynomial.X i +
                    -c • HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X 0) (r i)) :
            (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          (MvPolynomial.X i)))
      (MvPolynomial.coeff v
        ((MvPolynomial.aeval MvPolynomial.X : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          (MvPolynomial.X i)))
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin (n + 1)) k →ₐ[k] MvPolynomial (Fin (n + 1)) k)
    (MvPolynomial.aeval fun (i : Fin (n + 1)) ↦
      (T1 f c : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (if i = 0 then MvPolynomial.X 0
        else MvPolynomial.X i + -c • HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X 0) (r i)))
    (MvPolynomial.aeval MvPolynomial.X)

Tactic:
ext i v
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
i : Fin (n + 1)
v : Fin (n + 1) →₀ ℕ
hf :
  Eq.{u_1 + 1} (α := k)
    (MvPolynomial.coeff v
      ((MvPolynomial.aeval fun (i : Fin (n + 1)) ↦
            (T1 f c : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
              (if i = 0 then MvPolynomial.X 0
              else
                MvPolynomial.X i +
                  -c • HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X 0) (r i)) :
          (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (MvPolynomial.X 0)))
    (MvPolynomial.coeff v
      ((MvPolynomial.aeval MvPolynomial.X : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (MvPolynomial.X 0)))
hf₁ :
  ∀ (i : Fin n),
    Eq.{u_1 + 1} (α := k)
      (MvPolynomial.coeff v
        ((MvPolynomial.aeval fun (i : Fin (n + 1)) ↦
              (T1 f c : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
                (if i = 0 then MvPolynomial.X 0
                else
                  MvPolynomial.X i +
                    -c • HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X 0) (r i)) :
            (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          (MvPolynomial.X i.succ)))
      (MvPolynomial.coeff v
        ((MvPolynomial.aeval MvPolynomial.X : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          (MvPolynomial.X i.succ)))
⊢ Eq.{u_1 + 1} (α := k)
    (MvPolynomial.coeff v
      ((MvPolynomial.aeval fun (i : Fin (n + 1)) ↦
            (T1 f c : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
              (if i = 0 then MvPolynomial.X 0
              else
                MvPolynomial.X i +
                  -c • HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X 0) (r i)) :
          (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (MvPolynomial.X i)))
    (MvPolynomial.coeff v
      ((MvPolynomial.aeval MvPolynomial.X : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (MvPolynomial.X i)))

Tactic:
cases i using Fin.cases
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
v : Fin (n + 1) →₀ ℕ
⊢ Eq.{u_1 + 1} (α := k)
    (MvPolynomial.coeff v
      ((MvPolynomial.aeval fun (i : Fin (n + 1)) ↦
            (T1 f c : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
              (if i = 0 then MvPolynomial.X 0
              else
                MvPolynomial.X i +
                  -c • HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X 0) (r i)) :
          (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (MvPolynomial.X 0)))
    (MvPolynomial.coeff v
      ((MvPolynomial.aeval MvPolynomial.X : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (MvPolynomial.X 0)))

Tactic:
simp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
v : Fin (n + 1) →₀ ℕ
i : Fin n
⊢ Eq.{u_1 + 1} (α := k)
    (MvPolynomial.coeff v
      ((MvPolynomial.aeval fun (i : Fin (n + 1)) ↦
            (T1 f c : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
              (if i = 0 then MvPolynomial.X 0
              else
                MvPolynomial.X i +
                  -c • HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X 0) (r i)) :
          (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (MvPolynomial.X i.succ)))
    (MvPolynomial.coeff v
      ((MvPolynomial.aeval MvPolynomial.X : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        (MvPolynomial.X i.succ)))

Tactic:
simp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
⊢ (T1 f (-1)).comp (T1 f 1) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Tactic:
simpa using t1_comp_t1_neg f (-1)

Premises used: _private.0.NoetherNormalization.t1_comp_t1_neg, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), (v : (a : Fin (n + 1)) → ℕ) i < up
wlt : ∀ (i : Fin (n + 1)), (w : (a : Fin (n + 1)) → ℕ) i < up
ne : v ≠ w
h :
  Eq (α := ℕ) (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((v : (a : Fin (n + 1)) → ℕ) x : ℕ))
    (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((w : (a : Fin (n + 1)) → ℕ) x : ℕ))
⊢ False

Tactic:
ne <| Finsupp.ext <| congrFun <| ofFn_inj.mp ?_

Premises used: Finsupp.ext, List.ofFn_inj, congrFun, Iff.mp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), (v : (a : Fin (n + 1)) → ℕ) i < up
wlt : ∀ (i : Fin (n + 1)), (w : (a : Fin (n + 1)) → ℕ) i < up
ne : v ≠ w
h :
  Eq (α := ℕ) (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((v : (a : Fin (n + 1)) → ℕ) x : ℕ))
    (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((w : (a : Fin (n + 1)) → ℕ) x : ℕ))
refine :
  Eq (α := List ℕ) (ofFn (n := n + 1) (⇑v : (a : Fin (n + 1)) → ℕ)) (ofFn (n := n + 1) (⇑w : (a : Fin (n + 1)) → ℕ))
⊢ False

Tactic:
refine ne <| Finsupp.ext <| congrFun <| ofFn_inj.mp ?_

Premises used: Finsupp.ext, List.ofFn_inj, congrFun, Iff.mp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), (v : (a : Fin (n + 1)) → ℕ) i < up
wlt : ∀ (i : Fin (n + 1)), (w : (a : Fin (n + 1)) → ℕ) i < up
ne : v ≠ w
h :
  Eq (α := ℕ) (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((v : (a : Fin (n + 1)) → ℕ) x : ℕ))
    (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((w : (a : Fin (n + 1)) → ℕ) x : ℕ))
⊢ length (α := ℕ) (ofFn (n := n + 1) (⇑v : (a : Fin (n + 1)) → ℕ)) =
    length (α := ℕ) (ofFn (n := n + 1) (⇑w : (a : Fin (n + 1)) → ℕ))

Tactic:
simp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), (v : (a : Fin (n + 1)) → ℕ) i < up
wlt : ∀ (i : Fin (n + 1)), (w : (a : Fin (n + 1)) → ℕ) i < up
ne : v ≠ w
h :
  Eq (α := ℕ) (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((v : (a : Fin (n + 1)) → ℕ) x : ℕ))
    (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((w : (a : Fin (n + 1)) → ℕ) x : ℕ))
apply :
  ofDigits up (ofFn (n := n + 1) (⇑v : (a : Fin (n + 1)) → ℕ)) =
    ofDigits up (ofFn (n := n + 1) (⇑w : (a : Fin (n + 1)) → ℕ))
⊢ Eq (α := List ℕ) (ofFn (n := n + 1) (⇑v : (a : Fin (n + 1)) → ℕ)) (ofFn (n := n + 1) (⇑w : (a : Fin (n + 1)) → ℕ))

Tactic:
apply ofDigits_inj_of_len_eq (Nat.lt_add_right f.totalDegree one_lt_two)
    (by simp) (lt_up vlt) (lt_up wlt)

Premises used: _private.0.NoetherNormalization.lt_up, Nat.ofDigits_inj_of_len_eq, MvPolynomial.totalDegree, one_lt_two, Nat.lt_add_right
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
vlt : ∀ (i : Fin (n + 1)), (v : (a : Fin (n + 1)) → ℕ) i < up
wlt : ∀ (i : Fin (n + 1)), (w : (a : Fin (n + 1)) → ℕ) i < up
ne : v ≠ w
h :
  Eq (α := ℕ) (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((v : (a : Fin (n + 1)) → ℕ) x : ℕ))
    (∑ x : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r x : ℕ) ((w : (a : Fin (n + 1)) → ℕ) x : ℕ))
⊢ ofDigits up (ofFn (n := n + 1) (⇑v : (a : Fin (n + 1)) → ℕ)) =
    ofDigits up (ofFn (n := n + 1) (⇑w : (a : Fin (n + 1)) → ℕ))

Tactic:
simpa only [ofDigits_eq_sum_mapIdx, mapIdx_eq_ofFn, get_ofFn, length_ofFn,
    Fin.val_cast, mul_comm, sum_ofFn] using h

Premises used: List.get_ofFn, List.sum_ofFn, Nat.ofDigits_eq_sum_mapIdx, List.length_ofFn, mul_comm, Fin.val_cast, List.mapIdx_eq_ofFn
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
rw :
  natDegree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          (HMul.hMul (α := MvPolynomial (Fin (n + 1)) k) (β := MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) a : MvPolynomial (Fin (n + 1)) k)
            (∏ a : Fin (n + 1),
                HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X a)
                  ((v : (a : Fin (n + 1)) → ℕ) a : ℕ) :
              MvPolynomial (Fin (n + 1)) k)))) =
    ∑ i : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r i : ℕ) ((v : (a : Fin (n + 1)) → ℕ) i : ℕ)
⊢ degreeOf.{u_1, 0} (R := k) (σ := Fin (n + 1)) 0
      ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) a)) =
    ∑ i : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r i : ℕ) ((v : (a : Fin (n + 1)) → ℕ) i : ℕ)

Tactic:
rw [← natDegree_finSuccEquiv, monomial_eq, Finsupp.prod_pow v fun a ↦ X a]

Premises used: MvPolynomial.natDegree_finSuccEquiv, MvPolynomial.X, Finsupp.prod_pow, MvPolynomial.monomial_eq
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
simp :
  (HMul.hMul (α := (MvPolynomial (Fin n) k)[X])
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
            ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) a) :
          (MvPolynomial (Fin n) k)[X])
        (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X ((v : (a : Fin (n + 1)) → ℕ) 0 : ℕ) *
          ∏ x : Fin n,
            HPow.hPow (β := ℕ)
              (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X])
                ((Polynomial.C : (a : MvPolynomial (Fin n) k) → (MvPolynomial (Fin n) k)[X]) (MvPolynomial.X x) :
                  (MvPolynomial (Fin n) k)[X])
                (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) Polynomial.X (up ^ (↑x.succ : ℕ))))
              ((v : (a : Fin (n + 1)) → ℕ) x.succ : ℕ))).natDegree =
    HMul.hMul (β := ℕ) (up ^ (↑0 : ℕ)) ((v : (a : Fin (n + 1)) → ℕ) 0 : ℕ) +
      ∑ i : Fin n, HMul.hMul (β := ℕ) (up ^ (↑i.succ : ℕ)) ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ)
⊢ natDegree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          (HMul.hMul (α := MvPolynomial (Fin (n + 1)) k) (β := MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) a : MvPolynomial (Fin (n + 1)) k)
            (∏ a : Fin (n + 1),
                HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X a)
                  ((v : (a : Fin (n + 1)) → ℕ) a : ℕ) :
              MvPolynomial (Fin (n + 1)) k)))) =
    ∑ i : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r i : ℕ) ((v : (a : Fin (n + 1)) → ℕ) i : ℕ)

Tactic:
simp only [Fin.prod_univ_succ, Fin.sum_univ_succ, map_mul, map_prod, map_pow,
    AlgEquiv.ofAlgHom_apply, MvPolynomial.aeval_C, MvPolynomial.aeval_X, if_pos, Fin.succ_ne_zero,
    ite_false, one_smul, map_add, finSuccEquiv_X_zero, finSuccEquiv_X_succ, algebraMap_eq]

Premises used: MvPolynomial.aeval_X, ite_false, map_add, map_pow, if_pos, map_prod, one_smul, map_mul, Fin.prod_univ_succ, MvPolynomial.finSuccEquiv_X_succ, MvPolynomial.algebraMap_eq, Fin.succ_ne_zero, MvPolynomial.aeval_C, AlgEquiv.ofAlgHom_apply, MvPolynomial.finSuccEquiv_X_zero, Fin.sum_univ_succ
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
i : Fin n
⊢ (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X])
        ((Polynomial.C : (a : MvPolynomial (Fin n) k) → (MvPolynomial (Fin n) k)[X]) (MvPolynomial.X i) :
          (MvPolynomial (Fin n) k)[X])
        (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X (r i.succ))).leadingCoeff ≠
    0

Tactic:
simp [add_comm, leadingCoeff_X_pow_add_C]

Premises used: Polynomial.leadingCoeff_X_pow_add_C, add_comm