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) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ∀ (i : 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 i) :
            (MvPolynomial (Fin n) k)[X])
          (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X (r i.succ)))
        ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ) ≠
      0

Tactic:
have h (i : Fin n) :
      (Polynomial.C (X (R := k) i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0 :=
    pow_ne_zero (v i.succ) (leadingCoeff_ne_zero.mp <| by simp [add_comm, leadingCoeff_X_pow_add_C])
-- 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
h :
  ∀ (i : 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 i) :
            (MvPolynomial (Fin n) k)[X])
          (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X (r i.succ)))
        ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ) ≠
      0
⊢ Ne (α := (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])
    (0 : (MvPolynomial (Fin n) k)[X])

Tactic:
simp [ha]
-- 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
h :
  ∀ (i : 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 i) :
            (MvPolynomial (Fin n) k)[X])
          (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X (r i.succ)))
        ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ) ≠
      0
⊢ HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X ((v : (a : Fin (n + 1)) → ℕ) 0 : ℕ) ≠ 0

Tactic:
simp
-- 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
h :
  ∀ (i : 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 i) :
            (MvPolynomial (Fin n) k)[X])
          (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X (r i.succ)))
        ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ) ≠
      0
rw :
  0 +
      ((HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X
            ((v : (a : Fin (n + 1)) → ℕ) 0 : ℕ)).natDegree +
        ∑ i : 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 i) :
                  (MvPolynomial (Fin n) k)[X])
                (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X (r i.succ)))
              ((v : (a : Fin (n + 1)) → ℕ) i.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 : ℕ)
⊢ (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 : ℕ)

Tactic:
rw [natDegree_mul (by simp [ha]) (mul_ne_zero (by simp) (Finset.prod_ne_zero_iff.mpr
    (fun i _ ↦ h i))), natDegree_mul (by simp) (Finset.prod_ne_zero_iff.mpr (fun i _ ↦ h i)),
    natDegree_prod _ _ (fun i _ ↦ h i), natDegree_finSuccEquiv, degreeOf_C]

Premises used: Iff.mpr, MvPolynomial.natDegree_finSuccEquiv, MvPolynomial.degreeOf_C, Polynomial.natDegree_mul, Polynomial.natDegree_prod, Finset.prod_ne_zero_iff, mul_ne_zero
-- 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
h :
  ∀ (i : 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 i) :
            (MvPolynomial (Fin n) k)[X])
          (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X (r i.succ)))
        ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ) ≠
      0
i : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ i
rw :
  HMul.hMul (α := ℕ) ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ)
      (HAdd.hAdd (β := (MvPolynomial (Fin n) k)[X])
          (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) Polynomial.X (up ^ (↑i.succ : ℕ)))
          ((Polynomial.C : (a : MvPolynomial (Fin n) k) → (MvPolynomial (Fin n) k)[X]) (MvPolynomial.X i) :
            (MvPolynomial (Fin n) k)[X])).natDegree =
    HMul.hMul (β := ℕ) (up ^ (↑i.succ : ℕ)) ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ)
rw₁ :
  HMul.hMul (α := ℕ) ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ) (up ^ (↑i.succ : ℕ)) =
    HMul.hMul (β := ℕ) (up ^ (↑i.succ : ℕ)) ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ)
rw₂ rw₃ :
  HMul.hMul (β := ℕ) (up ^ (↑i.succ : ℕ)) ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ) =
    HMul.hMul (β := ℕ) (up ^ (↑i.succ : ℕ)) ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ)
⊢ HMul.hMul (α := ℕ) ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ)
      (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 (up ^ (↑i.succ : ℕ)))).natDegree =
    HMul.hMul (β := ℕ) (up ^ (↑i.succ : ℕ)) ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ)

Tactic:
rw [add_comm (Polynomial.C _), natDegree_X_pow_add_C, mul_comm]

Premises used: Polynomial.C, Polynomial.natDegree_X_pow_add_C, add_comm, mul_comm, DFunLike.coe
-- 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
h :
  ∀ (i : 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 i) :
            (MvPolynomial (Fin n) k)[X])
          (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X (r i.succ)))
        ((v : (a : Fin (n + 1)) → ℕ) i.succ : ℕ) ≠
      0
⊢ 0 +
      ((HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X
            ((v : (a : Fin (n + 1)) → ℕ) 0 : ℕ)).natDegree +
        ∑ i : 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 i) :
                  (MvPolynomial (Fin n) k)[X])
                (HPow.hPow (α := (MvPolynomial (Fin n) k)[X]) (β := ℕ) Polynomial.X (r i.succ)))
              ((v : (a : Fin (n + 1)) → ℕ) i.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 : ℕ)

Tactic:
simpa only [natDegree_pow, zero_add, natDegree_X, mul_one, Fin.val_zero, pow_zero, one_mul,
    add_right_inj] using Finset.sum_congr rfl (fun i _ ↦ by
    rw [add_comm (Polynomial.C _), natDegree_X_pow_add_C, mul_comm])

Premises used: Polynomial.natDegree_X, zero_add, pow_zero, Polynomial.natDegree_pow, mul_one, Fin.val_zero, add_right_inj, Finset.sum_congr, one_mul, 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) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
rw :
  Ne (α := ℕ) (∑ i : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r i : ℕ) ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))
    (∑ i : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r i : ℕ) ((w : (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) (MvPolynomial.coeff v 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 w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)))

Tactic:
rw [degreeOf_zero_t _ _ <| mem_support_iff.mp hv, degreeOf_zero_t _ _ <| mem_support_iff.mp hw]

Premises used: MvPolynomial.mem_support_iff, _private.0.NoetherNormalization.degreeOf_zero_t, 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) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
⊢ Ne (α := ℕ) (∑ i : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r i : ℕ) ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))
    (∑ i : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r i : ℕ) ((w : (a : Fin (n + 1)) → ℕ) i : ℕ))

Tactic:
sum_r_mul_ne f v w (fun i ↦ ?_) (fun i ↦ ?_) ne

Premises used: _private.0.NoetherNormalization.sum_r_mul_ne
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
refine_1 : ∀ (i : Fin (n + 1)), (v : (a : Fin (n + 1)) → ℕ) i < up
refine_2 : ∀ (i : Fin (n + 1)), (w : (a : Fin (n + 1)) → ℕ) i < up
⊢ Ne (α := ℕ) (∑ i : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r i : ℕ) ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))
    (∑ i : Fin (n + 1), HMul.hMul (α := ℕ) (β := ℕ) (r i : ℕ) ((w : (a : Fin (n + 1)) → ℕ) i : ℕ))

Tactic:
refine sum_r_mul_ne f v w (fun i ↦ ?_) (fun i ↦ ?_) ne

Premises used: _private.0.NoetherNormalization.sum_r_mul_ne
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ f.totalDegree < up

Tactic:
lia
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ (v : (a : Fin (n + 1)) → ℕ) i < up

Tactic:
exact lt_of_le_of_lt ((monomial_le_degreeOf i ‹_›).trans (degreeOf_le_totalDegree f i))
    (by lia)

Premises used: lt_of_le_of_lt, MvPolynomial.degreeOf_le_totalDegree, MvPolynomial.monomial_le_degreeOf, LE.le.trans
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v w : Fin (n + 1) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
i : Fin (n + 1)
⊢ (w : (a : Fin (n + 1)) → ℕ) i < up

Tactic:
exact lt_of_le_of_lt ((monomial_le_degreeOf i ‹_›).trans (degreeOf_le_totalDegree f i))
    (by lia)

Premises used: lt_of_le_of_lt, MvPolynomial.degreeOf_le_totalDegree, MvPolynomial.monomial_le_degreeOf, LE.le.trans
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
rw :
  Eq (α := 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)
            (HMul.hMul (α := MvPolynomial (Fin (n + 1)) k) (β := MvPolynomial (Fin (n + 1)) k)
              ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f) :
                MvPolynomial (Fin (n + 1)) k)
              (∏ i : Fin (n + 1),
                  HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                    ((v : (a : Fin (n + 1)) → ℕ) i : ℕ) :
                MvPolynomial (Fin (n + 1)) k)))) :
      MvPolynomial (Fin n) k)
    ((algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) :
      MvPolynomial (Fin n) k)
h : ∀ (i : Fin (n + 1)), HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i) 0 = 1
⊢ Eq (α := 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)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))) :
      MvPolynomial (Fin n) k)
    ((algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) :
      MvPolynomial (Fin n) k)

Tactic:
rw [monomial_eq, Finsupp.prod_fintype]

Premises used: MvPolynomial.monomial_eq, Finsupp.prod_fintype
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
simp :
  HMul.hMul (α := 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)
            ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))))
      (∏ i : Fin (n + 1),
        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)
              (HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))))) =
    (algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)
⊢ Eq (α := 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)
            (HMul.hMul (α := MvPolynomial (Fin (n + 1)) k) (β := MvPolynomial (Fin (n + 1)) k)
              ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f) :
                MvPolynomial (Fin (n + 1)) k)
              (∏ i : Fin (n + 1),
                  HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                    ((v : (a : Fin (n + 1)) → ℕ) i : ℕ) :
                MvPolynomial (Fin (n + 1)) k)))) :
      MvPolynomial (Fin n) k)
    ((algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) :
      MvPolynomial (Fin n) k)

Tactic:
simp only [map_mul, map_prod, leadingCoeff_mul, leadingCoeff_prod]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.leadingCoeff_prod, map_prod, map_mul
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
rw :
  HMul.hMul (α := MvPolynomial (Fin n) k)
      (Polynomial.leadingCoeff
        (Function.comp (β := MvPolynomial (Fin n) k)
          (⇑Polynomial.C : (a : MvPolynomial (Fin n) k) → (MvPolynomial (Fin n) k)[X])
          (⇑MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)))
      (∏ i : Fin (n + 1),
        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)
              (HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))))) =
    (algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)
⊢ HMul.hMul (α := 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)
            ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))))
      (∏ i : Fin (n + 1),
        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)
              (HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))))) =
    (algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)

Tactic:
rw [AlgEquiv.ofAlgHom_apply, algHom_C, algebraMap_eq, finSuccEquiv_apply,
      eval₂Hom_C, coe_comp]

Premises used: MvPolynomial.algHom_C, MvPolynomial.finSuccEquiv_apply, MvPolynomial.algebraMap_eq, RingHom.coe_comp, AlgEquiv.ofAlgHom_apply, MvPolynomial.eval₂Hom_C
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
simp :
  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)
⊢ HMul.hMul (α := MvPolynomial (Fin n) k)
      (Polynomial.leadingCoeff
        (Function.comp (β := MvPolynomial (Fin n) k)
          (⇑Polynomial.C : (a : MvPolynomial (Fin n) k) → (MvPolynomial (Fin n) k)[X])
          (⇑MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)))
      (∏ i : Fin (n + 1),
        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)
              (HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))))) =
    (algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)

Tactic:
simp only [AlgEquiv.ofAlgHom_apply, Function.comp_apply, leadingCoeff_C, map_pow,
      leadingCoeff_pow, algebraMap_eq]

Premises used: map_pow, MvPolynomial.algebraMap_eq, Function.comp_apply, AlgEquiv.ofAlgHom_apply, Polynomial.leadingCoeff_C, Polynomial.leadingCoeff_pow
-- 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)
pos :
  ∀ (h : j = 0),
    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
neg :
  ∀ (h : ¬j = 0),
    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
⊢ 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:
by_cases h : j = 0
-- 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
⊢ 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:
simp [h, finSuccEquiv_apply]

Premises used: MvPolynomial.finSuccEquiv_apply
-- 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 :
  (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
⊢ 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:
simp only [aeval_eq_bind₁, bind₁_X_right, if_neg h, one_smul, map_add, map_pow]

Premises used: map_add, map_pow, one_smul, MvPolynomial.aeval_eq_bind₁, MvPolynomial.bind₁_X_right, if_neg