awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ Eq (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))) :
      MvPolynomial (Fin n) k)
    ((algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) :
      MvPolynomial (Fin n) k)
have rw : Eq (α := MvPolynomial (Fin n) k)
  (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          (HMul.hMul (α := MvPolynomial (Fin (n + 1)) k) (β := MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f) :
              MvPolynomial (Fin (n + 1)) k)
            (∏ i : Fin (n + 1),
                HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                  ((v : (a : Fin (n + 1)) → ℕ) i : ℕ) :
              MvPolynomial (Fin (n + 1)) k)))) :
    MvPolynomial (Fin n) k)
  ((algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) :
    MvPolynomial (Fin n) k)
Tactic: rw [monomial_eq, Finsupp.prod_fintype]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
rw :
  Eq (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            (HMul.hMul (α := MvPolynomial (Fin (n + 1)) k) (β := MvPolynomial (Fin (n + 1)) k)
              ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f) :
                MvPolynomial (Fin (n + 1)) k)
              (∏ i : Fin (n + 1),
                  HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                    ((v : (a : Fin (n + 1)) → ℕ) i : ℕ) :
                MvPolynomial (Fin (n + 1)) k)))) :
      MvPolynomial (Fin n) k)
    ((algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) :
      MvPolynomial (Fin n) k)
⊢ Eq (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))) :
      MvPolynomial (Fin n) k)
    ((algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) :
      MvPolynomial (Fin n) k)
have h : ∀ (i : Fin (n + 1)), HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i) 0 = 1
Tactic: rw [monomial_eq, Finsupp.prod_fintype]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ Eq (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            (HMul.hMul (α := MvPolynomial (Fin (n + 1)) k) (β := MvPolynomial (Fin (n + 1)) k)
              ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f) :
                MvPolynomial (Fin (n + 1)) k)
              (∏ i : Fin (n + 1),
                  HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                    ((v : (a : Fin (n + 1)) → ℕ) i : ℕ) :
                MvPolynomial (Fin (n + 1)) k)))) :
      MvPolynomial (Fin n) k)
    ((algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) :
      MvPolynomial (Fin n) k)
have simp : HMul.hMul (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))))
    (∏ i : Fin (n + 1),
      Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            (HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
              ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))))) =
  (algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)
Tactic: simp only [map_mul, map_prod, leadingCoeff_mul, leadingCoeff_prod]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ HMul.hMul (α := MvPolynomial (Fin n) k)
      (Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.C : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))))
      (∏ i : Fin (n + 1),
        Polynomial.leadingCoeff
          ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
            ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
              (HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))))) =
    (algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)
have rw : HMul.hMul (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      (Function.comp (β := MvPolynomial (Fin n) k)
        (⇑Polynomial.C : (a : MvPolynomial (Fin n) k) → (MvPolynomial (Fin n) k)[X])
        (⇑MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)))
    (∏ i : Fin (n + 1),
      Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            (HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
              ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))))) =
  (algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)
Tactic: rw [AlgEquiv.ofAlgHom_apply, algHom_C, algebraMap_eq, finSuccEquiv_apply,
      eval₂Hom_C, coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ HMul.hMul (α := MvPolynomial (Fin n) k)
      (Polynomial.leadingCoeff
        (Function.comp (β := MvPolynomial (Fin n) k)
          (⇑Polynomial.C : (a : MvPolynomial (Fin n) k) → (MvPolynomial (Fin n) k)[X])
          (⇑MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)))
      (∏ i : Fin (n + 1),
        Polynomial.leadingCoeff
          ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
            ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
              (HPow.hPow (α := MvPolynomial (Fin (n + 1)) k) (β := ℕ) (MvPolynomial.X i)
                ((v : (a : Fin (n + 1)) → ℕ) i : ℕ))))) =
    (algebraMap k (MvPolynomial (Fin n) k) : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)
have simp : HMul.hMul (α := MvPolynomial (Fin n) k) (β := MvPolynomial (Fin n) k)
    ((MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) : MvPolynomial (Fin n) k)
    (∏ x : Fin (n + 1),
        HPow.hPow (α := MvPolynomial (Fin n) k) (β := ℕ)
          (Polynomial.leadingCoeff
            ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
              ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X x))))
          ((v : (a : Fin (n + 1)) → ℕ) x : ℕ) :
      MvPolynomial (Fin n) k) =
  (MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)
Tactic: simp only [AlgEquiv.ofAlgHom_apply, Function.comp_apply, leadingCoeff_C, map_pow,
      leadingCoeff_pow, algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X j))))
    1
have pos : ∀ (h : j = 0),
  Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X j))))
    1
Tactic: by_cases h : j = 0
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
pos :
  ∀ (h : j = 0),
    Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
      (Polynomial.leadingCoeff
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X j))))
      1
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X j))))
    1
have neg : ∀ (h : ¬j = 0),
  Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X j))))
    1
Tactic: by_cases h : j = 0
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : ¬j = 0
⊢ Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X j))))
    1
have neg : (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X])
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          (MvPolynomial.X j) :
        (MvPolynomial (Fin n) k)[X])
      (HPow.hPow (α := (MvPolynomial (Fin n) k)[X])
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
            (MvPolynomial.X 0) :
          (MvPolynomial (Fin n) k)[X])
        (up ^ (↑j : ℕ)))).leadingCoeff =
  1
Tactic: simp only [aeval_eq_bind₁, bind₁_X_right, if_neg h, one_smul, map_add, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : ¬j = 0
⊢ (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X])
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
            (MvPolynomial.X j) :
          (MvPolynomial (Fin n) k)[X])
        (HPow.hPow (α := (MvPolynomial (Fin n) k)[X])
          ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
              (MvPolynomial.X 0) :
            (MvPolynomial (Fin n) k)[X])
          (up ^ (↑j : ℕ)))).leadingCoeff =
    1
have neg : ∀ (i : Fin n) (h : ¬i.succ = 0),
  (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X])
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
            (MvPolynomial.X i.succ) :
          (MvPolynomial (Fin n) k)[X])
        (HPow.hPow (α := (MvPolynomial (Fin n) k)[X])
          ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
              (MvPolynomial.X 0) :
            (MvPolynomial (Fin n) k)[X])
          (up ^ (↑i.succ : ℕ)))).leadingCoeff =
    1
Tactic: obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ HMul.hMul (α := MvPolynomial (Fin n) k) (β := MvPolynomial (Fin n) k)
      ((MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f) : MvPolynomial (Fin n) k)
      (∏ x : Fin (n + 1),
          HPow.hPow (α := MvPolynomial (Fin n) k) (β := ℕ)
            (Polynomial.leadingCoeff
              ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
                ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X x))))
            ((v : (a : Fin (n + 1)) → ℕ) x : ℕ) :
        MvPolynomial (Fin n) k) =
    (MvPolynomial.C : (a : k) → MvPolynomial (Fin n) k) (MvPolynomial.coeff v f)
have this : ∀ (j : Fin (n + 1)),
  Eq.{u_1 + 1} (α := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T1 f 1 : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.X j))))
    1
Tactic: have : ∀ j, ((finSuccEquiv k n) ((T1 f) 1 (X j))).leadingCoeff = 1 := fun j ↦ by
      by_cases h : j = 0
      · simp [h, finSuccEquiv_apply]
      · simp only [aeval_eq_bind₁, bind₁_X_right, if_neg h, one_smul, map_add, map_pow]
        obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h
        simp [finSuccEquiv_X_succ, finSuccEquiv_X_zero, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
fne : f ≠ 0
⊢ IsUnit.{u_1} (M := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) f)))
have obtain : ∀ (v : Fin (n + 1) →₀ ℕ) (vin : v ∈ f.support)
  (vs :
    ∀ x' ∈ f.support,
      degreeOf.{u_1, 0} (R := k) (σ := Fin (n + 1)) 0
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f))) ≤
        degreeOf.{u_1, 0} (R := k) (σ := Fin (n + 1)) 0
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))),
  IsUnit.{u_1} (M := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) f)))
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)
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
Goal:
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.{u_1, 0} (R := k) (σ := Fin (n + 1)) 0
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f))) ≤
      degreeOf.{u_1, 0} (R := k) (σ := Fin (n + 1)) 0
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))
h : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
⊢ IsUnit.{u_1} (M := MvPolynomial (Fin n) k)
    (Polynomial.leadingCoeff
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) f)))
have vs₁ : ∀ x' ∈ f.support,
  natDegree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
    natDegree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
          ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
Tactic: simp only [← natDegree_finSuccEquiv] at vs
Cleared hypotheses: vs
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
Goal:
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 : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    natDegree.{u_1} (R := MvPolynomial (Fin n) k)
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
      natDegree.{u_1} (R := MvPolynomial (Fin n) k)
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
⊢ degree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h x))) <
    degree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h v)))
have h1 : x ∈ f.support
Tactic: obtain ⟨h1, h2⟩ := Finset.mem_sdiff.mp hx
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
Goal:
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 : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    natDegree.{u_1} (R := MvPolynomial (Fin n) k)
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
      natDegree.{u_1} (R := MvPolynomial (Fin n) k)
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
h1 : x ∈ f.support
⊢ degree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h x))) <
    degree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h v)))
have h2 : x ∉ {v}
Tactic: obtain ⟨h1, h2⟩ := Finset.mem_sdiff.mp hx
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (goal)
Goal:
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 : (w : Fin (n + 1) →₀ ℕ) → MvPolynomial (Fin (n + 1)) k :=
  fun (w : Fin (n + 1) →₀ ℕ) ↦
    (MvPolynomial.monomial w : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff w f)
vs :
  ∀ x' ∈ f.support,
    natDegree.{u_1} (R := MvPolynomial (Fin n) k)
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial x' : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x' f)))) ≤
      natDegree.{u_1} (R := MvPolynomial (Fin n) k)
        ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
          ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
            ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
x : Fin (n + 1) →₀ ℕ
hx : x ∈ f.support \ {v}
h1 : x ∈ f.support
h2 : x ∉ {v}
⊢ degree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h x))) <
    degree.{u_1} (R := MvPolynomial (Fin n) k)
      ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h v)))
have apply : natDegree.{u_1} (R := MvPolynomial (Fin n) k)
    ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
      ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        ((MvPolynomial.monomial x : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff x f)))) ≠
  natDegree.{u_1} (R := MvPolynomial (Fin n) k)
    ((MvPolynomial.finSuccEquiv k n : (a : MvPolynomial (Fin (n + 1)) k) → (MvPolynomial (Fin n) k)[X])
      ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k)
        ((MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f))))
Tactic: apply degree_lt_degree <| lt_of_le_of_ne (vs x h1) ?_