-- 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 : 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

Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_sdiff.mp hx

Result:
case 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
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
h1 : x ∈ f.support
h2 : x ∉ {v}
⊢ ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x))).degree <
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).degree

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}, h x))).leadingCoeff =
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).leadingCoeff

Tactic:
simp only [map_add, map_sum]

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
⊢ ((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

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
⊢ (∑ 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

Tactic:
apply leadingCoeff_add_of_degree_lt <| (lt_of_le_of_lt <| degree_sum_le _ _) ?_

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
⊢ ((f.support \ {v}).sup fun b => ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h b))).degree) <
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).degree

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
h2 : h v ≠ 0
eq : (MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v)) = 0
⊢ h v = 0

Tactic:
simpa only [map_eq_zero_iff _ (AlgEquiv.injective _)] using eq

Result:
no goals

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,
    ((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

Tactic:
replace vs : ∀ x ∈ f.support \ {v}, (finSuccEquiv k n ((T f) (h x))).degree <
    (finSuccEquiv k n ((T f) (h v))).degree := by
  intro x hx
  obtain ⟨h1, h2⟩ := Finset.mem_sdiff.mp hx
  apply degree_lt_degree <| lt_of_le_of_ne (vs x h1) ?_
  simpa only [natDegree_finSuccEquiv]
    using degreeOf_t_neq_of_neq f _ _ h1 vin <| ne_of_not_mem_cons h2

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
⊢ 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
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

Tactic:
simpa only [coeff, algebraMap_eq] using (mem_support_iff.mp vin).isUnit.map MvPolynomial.C

Result:
no goals