-- Mathlib/RingTheory/NoetherNormalization.lean
private lemma degreeOf_zero_t {a : k} (ha : a ≠ 0) : ((T f) (monomial v a)).degreeOf 0 =
    ∑ i : Fin (n + 1), (r i) * v i

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ degreeOf 0 ((NoetherNormalization.T f) ((MvPolynomial.monomial v) a)) = ∑ i : Fin (n + 1), r i * v i

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

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n)
        ((NoetherNormalization.T f) (MvPolynomial.C a * ∏ a : Fin (n + 1), MvPolynomial.X a ^ v a))).natDegree =
    ∑ i : Fin (n + 1), r i * v i

Proof state:
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), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ Polynomial.X ^ v 0 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
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), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
i : Fin n
x✝ : i ∈ Finset.univ
⊢ v i.succ * (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ up ^ ↑i.succ).natDegree = up ^ ↑i.succ * v i.succ

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

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n)
        ((NoetherNormalization.T f) (MvPolynomial.C a * ∏ a : Fin (n + 1), MvPolynomial.X a ^ v a))).natDegree =
    ∑ i : Fin (n + 1), r i * v i

Tactic:
simp only [Fin.prod_univ_succ, Fin.sum_univ_succ, _root_.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]

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.C a) *
        (Polynomial.X ^ v 0 *
          ∏ x : Fin n, (Polynomial.C (MvPolynomial.X x) + Polynomial.X ^ up ^ ↑x.succ) ^ v x.succ)).natDegree =
    up ^ ↑0 * v 0 + ∑ i : Fin n, up ^ ↑i.succ * v i.succ

Proof state:
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), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ 0 +
      ((Polynomial.X ^ v 0).natDegree +
        ∑ i : Fin n, ((Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ).natDegree) =
    up ^ ↑0 * v 0 + ∑ i : Fin n, up ^ ↑i.succ * v 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])

Result:
no goals

Proof state:
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
⊢ (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ).leadingCoeff ≠ 0

Tactic:
simp [add_comm, leadingCoeff_X_pow_add_C]

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
a : k
ha : a ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.C a) *
        (Polynomial.X ^ v 0 *
          ∏ x : Fin n, (Polynomial.C (MvPolynomial.X x) + Polynomial.X ^ up ^ ↑x.succ) ^ v x.succ)).natDegree =
    up ^ ↑0 * v 0 + ∑ i : Fin n, up ^ ↑i.succ * v i.succ

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])

Result:
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), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.C a) *
        (Polynomial.X ^ v 0 *
          ∏ x : Fin n, (Polynomial.C (MvPolynomial.X x) + Polynomial.X ^ up ^ ↑x.succ) ^ v x.succ)).natDegree =
    up ^ ↑0 * v 0 + ∑ i : Fin n, up ^ ↑i.succ * v i.succ

Proof state:
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), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ (MvPolynomial.finSuccEquiv k n) (MvPolynomial.C a) ≠ 0

Tactic:
simp [ha]

Result:
no goals

Proof state:
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), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.C a) *
        (Polynomial.X ^ v 0 *
          ∏ x : Fin n, (Polynomial.C (MvPolynomial.X x) + Polynomial.X ^ up ^ ↑x.succ) ^ v x.succ)).natDegree =
    up ^ ↑0 * v 0 + ∑ i : Fin n, up ^ ↑i.succ * v 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]

Result:
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), (Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ ≠ 0
⊢ 0 +
      ((Polynomial.X ^ v 0).natDegree +
        ∑ i : Fin n, ((Polynomial.C (MvPolynomial.X i) + Polynomial.X ^ r i.succ) ^ v i.succ).natDegree) =
    up ^ ↑0 * v 0 + ∑ i : Fin n, up ^ ↑i.succ * v i.succ