-- Mathlib/RingTheory/NoetherNormalization.lean
private lemma T_leadingcoeff_isUnit (fne : f ≠ 0) :
    IsUnit (finSuccEquiv k n (T f f)).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
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) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff

Tactic:
rw [leadingCoeff_finSuccEquiv_t] at 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 =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v + ∑ x ∈ f.support \ {v}, h x))).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
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

Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton vin h]

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) (h v + ∑ x ∈ f.support \ {v}, h x))).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)))
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

Tactic:
simp only [← natDegree_finSuccEquiv] at vs

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,
    ((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
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) f)).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
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
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) f)).leadingCoeff

Tactic:
have coeff : (finSuccEquiv k n ((T f) (h v + ∑ x ∈ f.support \ {v}, h x))).leadingCoeff =
    (finSuccEquiv k n ((T f) (h v))).leadingCoeff := by
  simp only [map_add, map_sum]
  rw [add_comm]
  apply leadingCoeff_add_of_degree_lt <| (lt_of_le_of_lt <| degree_sum_le _ _) ?_
  have h2 : h v ≠ 0 := by simpa [h] using mem_support_iff.mp vin
  replace h2 : (finSuccEquiv k n ((T f) (h v))) ≠ 0 := fun eq ↦ h2 <|
    by simpa only [map_eq_zero_iff _ (AlgEquiv.injective _)] using eq
  exact (Finset.sup_lt_iff <| Ne.bot_lt (fun x ↦ h2 <| degree_eq_bot.mp x)).mpr vs

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) f)).leadingCoeff