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 : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : ¬j = 0
neg :
  ∀ (i : Fin n) (h : ¬i.succ = 0),
    (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X])
          ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
              (MvPolynomial.X i.succ) :
            (MvPolynomial (Fin n) k)[X])
          (HPow.hPow (α := (MvPolynomial (Fin n) k)[X])
            ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
                (MvPolynomial.X 0) :
              (MvPolynomial (Fin n) k)[X])
            (up ^ (↑i.succ : ℕ)))).leadingCoeff =
      1
⊢ (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X])
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
            (MvPolynomial.X j) :
          (MvPolynomial (Fin n) k)[X])
        (HPow.hPow (α := (MvPolynomial (Fin n) k)[X])
          ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
              (MvPolynomial.X 0) :
            (MvPolynomial (Fin n) k)[X])
          (up ^ (↑j : ℕ)))).leadingCoeff =
    1

Tactic:
obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h

Premises used: Iff.mpr, Fin.exists_succ_eq, rfl
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
i : Fin n
h : ¬i.succ = 0
⊢ (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X])
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
            (MvPolynomial.X i.succ) :
          (MvPolynomial (Fin n) k)[X])
        (HPow.hPow (α := (MvPolynomial (Fin n) k)[X])
          ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
              (MvPolynomial.X 0) :
            (MvPolynomial (Fin n) k)[X])
          (up ^ (↑i.succ : ℕ)))).leadingCoeff =
    1

Tactic:
simp [finSuccEquiv_X_succ, finSuccEquiv_X_zero, add_comm]

Premises used: add_comm, MvPolynomial.finSuccEquiv_X_succ, MvPolynomial.finSuccEquiv_X_zero
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (j : Fin (n + 1)),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
      (Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X j))))
      1

Tactic:
have : ∀ j, ((finSuccEquiv k n) ((T1 f) 1 (X j))).leadingCoeff = 1 := fun j ↦ by
      by_cases h : j = 0
      · simp [h, finSuccEquiv_apply]
      · simp only [aeval_eq_bind₁, bind₁_X_right, if_neg h, one_smul, map_add, map_pow]
        obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h
        simp [finSuccEquiv_X_succ, finSuccEquiv_X_zero, add_comm]
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
this :
  ∀ (j : Fin (n + 1)),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
      (Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X j))))
      1
⊢ HMul.hMul (α := MvPolynomial (Fin n) k) (β := MvPolynomial (Fin n) k)
      ((MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) : MvPolynomial (Fin n) k)
      (∏ x : Fin (n + 1),
          HPow.hPow (α := MvPolynomial (Fin n) k) (β := ℕ)
            (Polynomial.leadingCoeff
              ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
                ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X x))))
            ((v : (a : Fin (n + 1)) → ℕ) x : ℕ) :
        MvPolynomial (Fin n) k) =
    (MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)

Tactic:
simp only [this, one_pow, Finset.prod_const_one, mul_one]

Premises used: one_pow, Finset.prod_const_one, mul_one
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (i : Fin (n + 1)), HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i) 0 = 1

Tactic:
fun i ↦ pow_zero _

Premises used: MvPolynomial.X, pow_zero
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (i : Fin (n + 1)), HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i) 0 = 1

Tactic:
exact fun i ↦ pow_zero _

Premises used: pow_zero
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
obtain :
  ∀ (v : Fin (n + 1) →₀ ℕ) (vin : v ∈ f.support)
    (vs :
      ∀ x' ∈ f.support,
        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 x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f))) ≤
          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) (MvPolynomial.coeff v f)))),
    IsUnit.{u_1} (M := MvPolynomial (Fin n) k)
      (Polynomial.leadingCoeff
        ((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) f)))
⊢ IsUnit.{u_1} (M := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((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) f)))

Tactic:
obtain ⟨v, vin, vs⟩ := Finset.exists_max_image f.support
    (fun v ↦ (T f ((monomial v) (coeff v f))).degreeOf 0) (support_nonempty.mpr fne)

Premises used: Iff.mpr, MvPolynomial.monomial, Finset.exists_max_image, MvPolynomial.support, MvPolynomial.coeff, MvPolynomial.support_nonempty, OfNat.ofNat, DFunLike.coe, _private.0.NoetherNormalization.T, MvPolynomial.degreeOf
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
vs :
  ∀ x' ∈ f.support,
    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 x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f))) ≤
      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) (MvPolynomial.coeff v f)))
h : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
⊢ ∀ x' ∈ f.support,
    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)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
      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)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))

Tactic:
simp only [← natDegree_finSuccEquiv] at vs

Premises used: MvPolynomial.natDegree_finSuccEquiv
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    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)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
      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)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
⊢ x ∈ f.support

Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_sdiff.mp hx

Premises used: Finset.mem_sdiff, Iff.mp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    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)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
      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)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
h1 : x ∈ f.support
⊢ x ∉ {v}

Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_sdiff.mp hx

Premises used: Finset.mem_sdiff, Iff.mp
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    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)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
      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)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
h1 : x ∈ f.support
h2 : x ∉ {v}
apply :
  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)
          ((MvPolynomial.monomial x : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x f)))) ≠
    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)
          ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
⊢ degree.{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) (h x))) <
    degree.{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) (h v)))

Tactic:
apply degree_lt_degree <| lt_of_le_of_ne (vs x h1) ?_

Premises used: Polynomial.degree_lt_degree, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    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)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
      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)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
h1 : x ∈ f.support
h2 : x ∉ {v}
⊢ 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)
          ((MvPolynomial.monomial x : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x f)))) ≠
    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)
          ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))

Tactic:
simpa only [natDegree_finSuccEquiv]
      using degreeOf_t_ne_of_ne f _ _ h1 vin <| ne_of_not_mem_cons h2

Premises used: MvPolynomial.natDegree_finSuccEquiv, List.ne_of_not_mem_cons, _private.0.NoetherNormalization.degreeOf_t_ne_of_ne
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    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)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
      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)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
⊢ ∀ x ∈ f.support \ {v},
    degree.{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) (h x))) <
      degree.{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) (h v)))

Tactic:
replace vs : ∀ x ∈ f.support \ {v}, (finSuccEquiv k n ((T f) (h x))).degree <
      (finSuccEquiv k n ((T f) (h v))).degree := by
    intro x hx
    obtain ⟨h1, h2⟩ := Finset.mem_sdiff.mp hx
    apply degree_lt_degree <| lt_of_le_of_ne (vs x h1) ?_
    simpa only [natDegree_finSuccEquiv]
      using degreeOf_t_ne_of_ne f _ _ h1 vin <| ne_of_not_mem_cons h2
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    degree.{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) (h x))) <
      degree.{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) (h v)))
simp :
  (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X]) (β := (MvPolynomial (Fin n) k)[X])
        ((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) (h v)) :
          (MvPolynomial (Fin n) k)[X])
        (∑ x ∈ f.support \ {v},
            (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) (h x)) :
          (MvPolynomial (Fin n) k)[X])).leadingCoeff =
    Polynomial.leadingCoeff
      ((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) (h v)))
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((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) (h v + ∑ x ∈ f.support \ {v}, h x))))
    (Polynomial.leadingCoeff
      ((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) (h v))))

Tactic:
simp only [map_add, map_sum]

Premises used: map_add, map_sum
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
v : Fin (n + 1) →₀ ℕ
vin : v ∈ f.support
h : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    degree.{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) (h x))) <
      degree.{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) (h v)))
rw :
  (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X]) (β := (MvPolynomial (Fin n) k)[X])
        (∑ x ∈ f.support \ {v},
            (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) (h x)) :
          (MvPolynomial (Fin n) k)[X])
        ((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) (h v)) :
          (MvPolynomial (Fin n) k)[X])).leadingCoeff =
    Polynomial.leadingCoeff
      ((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) (h v)))
⊢ (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X]) (β := (MvPolynomial (Fin n) k)[X])
        ((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) (h v)) :
          (MvPolynomial (Fin n) k)[X])
        (∑ x ∈ f.support \ {v},
            (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) (h x)) :
          (MvPolynomial (Fin n) k)[X])).leadingCoeff =
    Polynomial.leadingCoeff
      ((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) (h v)))

Tactic:
rw [add_comm]

Premises used: add_comm