awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))))
⊢ 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 \ {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)))
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_ne_of_ne f _ _ h1 vin <| ne_of_not_mem_cons h2
Cleared hypotheses: vs
-- 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 \ {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)))
⊢ 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])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h v + ∑ x ∈ f.support \ {v}, h x))))
    (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) (h v))))
have simp : (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X]) (β := (MvPolynomial (Fin n) k)[X])
      ((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)) :
        (MvPolynomial (Fin n) k)[X])
      (∑ x ∈ f.support \ {v},
          (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)) :
        (MvPolynomial (Fin n) k)[X])).leadingCoeff =
  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) (h v)))
Tactic: simp only [map_add, map_sum]
-- 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 \ {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)))
⊢ (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X]) (β := (MvPolynomial (Fin n) k)[X])
        ((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)) :
          (MvPolynomial (Fin n) k)[X])
        (∑ x ∈ f.support \ {v},
            (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)) :
          (MvPolynomial (Fin n) k)[X])).leadingCoeff =
    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) (h v)))
have rw : (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X]) (β := (MvPolynomial (Fin n) k)[X])
      (∑ x ∈ f.support \ {v},
          (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)) :
        (MvPolynomial (Fin n) k)[X])
      ((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)) :
        (MvPolynomial (Fin n) k)[X])).leadingCoeff =
  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) (h v)))
Tactic: rw [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
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 \ {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)))
⊢ (HAdd.hAdd (α := (MvPolynomial (Fin n) k)[X]) (β := (MvPolynomial (Fin n) k)[X])
        (∑ x ∈ f.support \ {v},
            (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)) :
          (MvPolynomial (Fin n) k)[X])
        ((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)) :
          (MvPolynomial (Fin n) k)[X])).leadingCoeff =
    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) (h v)))
have apply : ((f.support \ {v}).sup fun (b : Fin (n + 1) →₀ ℕ) ↦
    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 b)))) <
  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)))
Tactic: apply leadingCoeff_add_of_degree_lt <| (lt_of_le_of_lt <| degree_sum_le _ _) ?_
-- 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 \ {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)))
⊢ ((f.support \ {v}).sup fun (b : Fin (n + 1) →₀ ℕ) ↦
      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 b)))) <
    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 : h v ≠ 0
Tactic: have h2 : h v ≠ 0 := by simpa [h] using mem_support_iff.mp vin
-- 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 \ {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)))
h2 : h v ≠ 0
⊢ ((f.support \ {v}).sup fun (b : Fin (n + 1) →₀ ℕ) ↦
      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 b)))) <
    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₁ : Ne (α := (MvPolynomial (Fin n) k)[X])
  ((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)) :
    (MvPolynomial (Fin n) k)[X])
  (0 : (MvPolynomial (Fin n) k)[X])
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
Cleared hypotheses: h2
-- 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 \ {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)))
⊢ 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 coeff : 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])
      ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h v + ∑ x ∈ f.support \ {v}, h x))))
  (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) (h v))))
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
-- 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 \ {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)))
coeff :
  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])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h v + ∑ x ∈ f.support \ {v}, h x))))
    (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) (h v))))
⊢ 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 nth_rw : 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)
        (∑ v ∈ f.support,
          (MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))))
Tactic: nth_rw 2 [← f.support_sum_monomial_coeff]
-- 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 \ {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)))
coeff :
  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])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h v + ∑ x ∈ f.support \ {v}, h x))))
    (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) (h v))))
⊢ 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)
          (∑ v ∈ f.support,
            (MvPolynomial.monomial v : (a : k) → MvPolynomial (Fin (n + 1)) k) (MvPolynomial.coeff v f)))))
have rw : 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) (h v + ∑ x ∈ f.support \ {v}, h x))))
Tactic: rw [Finset.sum_eq_add_sum_diff_singleton_of_mem vin 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
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 \ {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)))
coeff :
  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])
        ((T f : (a : MvPolynomial (Fin (n + 1)) k) → MvPolynomial (Fin (n + 1)) k) (h v + ∑ x ∈ f.support \ {v}, h x))))
    (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) (h v))))
⊢ 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) (h v + ∑ x ∈ f.support \ {v}, h x))))
have coeff₁ : 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)
          (h v + ∑ x ∈ f.support \ {v}, h x))) :
    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 [leadingCoeff_finSuccEquiv_t] at coeff
Cleared hypotheses: coeff
-- Lean 4 proof step from Mathlib.RingTheory.NoetherNormalization (hypothesis)
Goal:
k : Type u_1
inst : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
I : Ideal (MvPolynomial (Fin (n + 1)) k)
fne : f ≠ 0
fi : f ∈ I
⊢ (hom1 f I).IsIntegral
have u : 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 u := T_leadingcoeff_isUnit f 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
v w : Fin (n + 1) →₀ ℕ
I : Ideal (MvPolynomial (Fin (n + 1)) k)
g : MvPolynomial (Fin (n + 1)) k ≃ₐ[k] (MvPolynomial (Fin n) k)[X] := MvPolynomial.finSuccEquiv k n
⊢ Eq (α := Ideal (MvPolynomial (Fin (n + 1)) k)) (Ideal.map (T f) I)
    (Ideal.map (R := (MvPolynomial (Fin n) k)[X]) (F := (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (↑g.symm : (MvPolynomial (Fin n) k)[X] →+* MvPolynomial (Fin (n + 1)) k)
      (Ideal.map (R := MvPolynomial (Fin (n + 1)) k) g (Ideal.map (T f) I)))
have this : g.symm.toRingEquiv.toRingHom.comp (↑g : MvPolynomial (Fin (n + 1)) k →+* (MvPolynomial (Fin n) k)[X]) =
  RingHom.id (MvPolynomial (Fin (n + 1)) k)
Tactic: have : g.symm.toRingEquiv.toRingHom.comp g = RingHom.id _ :=
    g.toRingEquiv.symm_toRingHom_comp_toRingHom