-- Mathlib/RingTheory/NoetherNormalization.lean
private lemma T_leadingcoeff_isUnit (fne : f ≠ 0) :
    IsUnit (finSuccEquiv k n (T f f)).leadingCoeff

Proof state:
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 : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w => (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    ((MvPolynomial.finSuccEquiv k n)
          ((NoetherNormalization.T f) ((MvPolynomial.monomial x') (MvPolynomial.coeff x' f)))).natDegree ≤
      ((MvPolynomial.finSuccEquiv k n)
          ((NoetherNormalization.T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).natDegree
⊢ ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x))).degree <
      ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).degree

Tactic:
intro x hx

Result:
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 : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w => (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    ((MvPolynomial.finSuccEquiv k n)
          ((NoetherNormalization.T f) ((MvPolynomial.monomial x') (MvPolynomial.coeff x' f)))).natDegree ≤
      ((MvPolynomial.finSuccEquiv k n)
          ((NoetherNormalization.T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).natDegree
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
⊢ ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x))).degree <
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).degree

Proof state:
case intro.intro
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 : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w => (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x))).degree <
      ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).degree
coeff :
  ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).leadingCoeff
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) f)).leadingCoeff

Tactic:
nth_rw 2 [← f.support_sum_monomial_coeff]

Result:
case intro.intro
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 : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w => (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x))).degree <
      ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).degree
coeff :
  ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).leadingCoeff
⊢ IsUnit
    ((MvPolynomial.finSuccEquiv k n)
        ((NoetherNormalization.T f) (∑ v ∈ f.support, (MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).leadingCoeff

Proof state:
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 : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w => (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x))).degree <
      ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).degree
⊢ ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v)) +
        ∑ x ∈ f.support \ {v}, (MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).leadingCoeff

Tactic:
rw [add_comm]

Result:
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 : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w => (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
vs :
  ∀ x ∈ f.support \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x))).degree <
      ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).degree
⊢ (∑ x ∈ f.support \ {v}, (MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x)) +
        (MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).leadingCoeff

Proof state:
case intro.intro
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 0 ((NoetherNormalization.T f) ((MvPolynomial.monomial x') (MvPolynomial.coeff x' f))) ≤
      degreeOf 0 ((NoetherNormalization.T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) f)).leadingCoeff

Tactic:
set h := fun w ↦ (MvPolynomial.monomial w) (coeff w f)

Result:
case intro.intro
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 0 ((NoetherNormalization.T f) ((MvPolynomial.monomial x') (MvPolynomial.coeff x' f))) ≤
      degreeOf 0 ((NoetherNormalization.T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))
h : (Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k := fun w => (MvPolynomial.monomial w) (MvPolynomial.coeff w f)
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) f)).leadingCoeff