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

Tactic:
replace h2 : (finSuccEquiv k n ((T f) (h v))) ≠ 0 := fun eq ↦ h2 <|
  by simpa only [map_eq_zero_iff _ (AlgEquiv.injective _)] using eq

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

Tactic:
have h2 : h v ≠ 0 := by simpa [h] using mem_support_iff.mp vin

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
h2 : h v ≠ 0
⊢ ((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:
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

Tactic:
apply degree_lt_degree <| lt_of_le_of_ne (vs x h1) ?_

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}
h1 : x ∈ f.support
h2 : x ∉ {v}
⊢ ((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

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
⊢ h v ≠ 0

Tactic:
simpa [h] using mem_support_iff.mp vin

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) f)).leadingCoeff

Tactic:
obtain ⟨v, vin, vs⟩ := Finset.exists_max_image f.support
  (fun v ↦ (T f ((monomial v) (coeff v f))).degreeOf 0) (support_nonempty.mpr fne)

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)))
⊢ IsUnit ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.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 \ {v},
    ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h x))).degree <
      ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v))).degree
h2 : (MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (h v)) ≠ 0
⊢ ((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

Tactic:
exact (Finset.sup_lt_iff <| Ne.bot_lt (fun x ↦ h2 <| degree_eq_bot.mp x)).mpr vs

Result:
no goals

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}
h1 : x ∈ f.support
h2 : x ∉ {v}
⊢ ((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

Tactic:
simpa only [natDegree_finSuccEquiv]
  using degreeOf_t_neq_of_neq f _ _ h1 vin <| ne_of_not_mem_cons h2

Result:
no goals