awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NoetherNormalization
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)))
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)))
⊢ (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:
apply leadingCoeff_add_of_degree_lt <| (lt_of_le_of_lt <| degree_sum_le _ _) ?_

Premises used: lt_of_le_of_lt, Polynomial.degree_sum_le, Polynomial.leadingCoeff_add_of_degree_lt
-- Module: Mathlib.RingTheory.NoetherNormalization
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)))
⊢ h v ≠ 0

Tactic:
simpa [h] using mem_support_iff.mp vin

Premises used: MvPolynomial.mem_support_iff, Iff.mp
-- Module: Mathlib.RingTheory.NoetherNormalization
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)))
⊢ h v ≠ 0

Tactic:
have h2 : h v ≠ 0 := by simpa [h] using mem_support_iff.mp vin
-- Module: Mathlib.RingTheory.NoetherNormalization
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
eq :
  Eq (α := (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])
⊢ h v = 0

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

Premises used: map_eq_zero_iff, AlgEquiv.injective
-- Module: Mathlib.RingTheory.NoetherNormalization
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
⊢ 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
-- Module: Mathlib.RingTheory.NoetherNormalization
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 :
  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])
⊢ ((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:
(Finset.sup_lt_iff <| Ne.bot_lt (fun x ↦ h2 <| degree_eq_bot.mp x)).mpr vs

Premises used: Iff.mpr, Finset.sup_lt_iff, Iff.mp, Polynomial.degree_eq_bot, Ne.bot_lt
-- Module: Mathlib.RingTheory.NoetherNormalization
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 :
  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])
⊢ ((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:
exact (Finset.sup_lt_iff <| Ne.bot_lt (fun x ↦ h2 <| degree_eq_bot.mp x)).mpr vs

Premises used: Iff.mpr, Finset.sup_lt_iff, Iff.mp, Polynomial.degree_eq_bot, Ne.bot_lt
-- Module: Mathlib.RingTheory.NoetherNormalization
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))))

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
-- Module: Mathlib.RingTheory.NoetherNormalization
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))))
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)))))
⊢ 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:
nth_rw 2 [← f.support_sum_monomial_coeff]

Premises used: MvPolynomial.support_sum_monomial_coeff
-- Module: Mathlib.RingTheory.NoetherNormalization
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))))
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))))
⊢ 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:
rw [Finset.sum_eq_add_sum_diff_singleton_of_mem vin h]

Premises used: Finset.sum_eq_add_sum_diff_singleton_of_mem
-- Module: Mathlib.RingTheory.NoetherNormalization
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))))
⊢ 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

Premises used: _private.0.NoetherNormalization.leadingCoeff_finSuccEquiv_t
-- Module: Mathlib.RingTheory.NoetherNormalization
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 (α := 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)
⊢ 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:
simpa only [coeff, algebraMap_eq] using (mem_support_iff.mp vin).isUnit.map MvPolynomial.C

Premises used: MvPolynomial.mem_support_iff, Ne.isUnit, MvPolynomial.algebraMap_eq, Iff.mp, IsUnit.map, MvPolynomial.C
-- Module: Mathlib.RingTheory.NoetherNormalization
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
⊢ 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

Premises used: _private.0.NoetherNormalization.T_leadingcoeff_isUnit
-- Module: Mathlib.RingTheory.NoetherNormalization
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
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)))
⊢ (hom1 f I).IsIntegral

Tactic:
(monic_of_isUnit_leadingCoeff_inv_smul u).quotient_isIntegral <|
    Submodule.smul_of_tower_mem _ u.unit⁻¹.val <| mem_map_of_mem _ <| mem_map_of_mem _ fi

Premises used: Units.val, Ideal.mem_map_of_mem, Polynomial.monic_of_isUnit_leadingCoeff_inv_smul, Polynomial.Monic.quotient_isIntegral, Inv.inv, IsUnit.unit, Submodule.smul_of_tower_mem
-- Module: Mathlib.RingTheory.NoetherNormalization
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
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)))
⊢ (hom1 f I).IsIntegral

Tactic:
exact (monic_of_isUnit_leadingCoeff_inv_smul u).quotient_isIntegral <|
    Submodule.smul_of_tower_mem _ u.unit⁻¹.val <| mem_map_of_mem _ <| mem_map_of_mem _ fi

Premises used: Units.val, Ideal.mem_map_of_mem, Polynomial.monic_of_isUnit_leadingCoeff_inv_smul, Polynomial.Monic.quotient_isIntegral, Inv.inv, IsUnit.unit, List.mem_map_of_mem, Submodule.smul_of_tower_mem