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
c : k
⊢ (T1 f c).comp (T1 f (-c)) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)
have 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)
Tactic: rw [comp_aeval, ← MvPolynomial.aeval_X_left]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ 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)
have 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)))
Tactic: ext i v
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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) →₀ ℕ
⊢ 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)))
have 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)))
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
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)))
⊢ 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)))
have 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)))
Tactic: cases i using Fin.cases
Cleared hypotheses: i
-- 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) →₀ ℕ
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
have refine : Eq (α := List ℕ) (ofFn (n := n + 1) (⇑v : (a : Fin (n + 1)) → ℕ)) (ofFn (n := n + 1) (⇑w : (a : Fin (n + 1)) → ℕ))
Tactic: refine ne <| Finsupp.ext <| congrFun <| ofFn_inj.mp ?_
-- 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) →₀ ℕ
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 : ℕ))
⊢ Eq (α := List ℕ) (ofFn (n := n + 1) (⇑v : (a : Fin (n + 1)) → ℕ)) (ofFn (n := n + 1) (⇑w : (a : Fin (n + 1)) → ℕ))
have apply : ofDigits up (ofFn (n := n + 1) (⇑v : (a : Fin (n + 1)) → ℕ)) =
  ofDigits up (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)
-- 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 : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: rw [← natDegree_finSuccEquiv, monomial_eq, Finsupp.prod_pow v fun a ↦ X a]
-- 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 : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ 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 : ℕ)
have 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 : ℕ)
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]
-- 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 : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ (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 : ℕ)
have 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
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])
-- 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 : 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
⊢ (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 : ℕ)
have 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 : ℕ)
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]
-- 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 : 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
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: rw [add_comm (Polynomial.C _), natDegree_X_pow_add_C, mul_comm]
-- 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 : 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 : ℕ)
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: rw [add_comm (Polynomial.C _), natDegree_X_pow_add_C, mul_comm]
-- 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 : 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 : ℕ)
⊢ 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 : ℕ)
have 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 : ℕ)
Tactic: rw [add_comm (Polynomial.C _), natDegree_X_pow_add_C, mul_comm]
-- 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) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
⊢ 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)))
have 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 : ℕ))
Tactic: rw [degreeOf_zero_t _ _ <| mem_support_iff.mp hv, degreeOf_zero_t _ _ <| mem_support_iff.mp hw]
-- 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) →₀ ℕ
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 : ℕ))
have refine_1 : ∀ (i : Fin (n + 1)), (v : (a : Fin (n + 1)) → ℕ) i < up
Tactic: refine sum_r_mul_ne f v w (fun i ↦ ?_) (fun i ↦ ?_) ne
-- 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) →₀ ℕ
hv : v ∈ f.support
hw : w ∈ f.support
ne : v ≠ w
refine_1 : ∀ (i : Fin (n + 1)), (v : (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 : ℕ))
have refine_2 : ∀ (i : Fin (n + 1)), (w : (a : Fin (n + 1)) → ℕ) i < up
Tactic: refine sum_r_mul_ne f v w (fun i ↦ ?_) (fun i ↦ ?_) ne