awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
q : MvPolynomial σ R :=
  (g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯)
h1 :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
refine : f = q * b + r
⊢ ∃ (g : MvPolynomial σ R) (r : MvPolynomial σ R),
    f = g * b + r ∧
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * g)) : m.syn)
          ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn) ∧
        ∀ c ∈ r.support, ¬m.degree b ≤ c

Tactic:
refine ⟨q, r, ?_, h1, h2⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
q : MvPolynomial σ R :=
  (g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯)
h1 :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
rw :
  HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r =
    q * b + r
⊢ f = q * b + r

Tactic:
rw [hgr]
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
q : MvPolynomial σ R :=
  (g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯)
h1 :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
simp : (g.sum fun (i : (↑{b} : Type (max u_1 u_2))) (c : MvPolynomial σ R) ↦ c * (↑i : MvPolynomial σ R)) = q * b
⊢ HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r =
    q * b + r

Tactic:
simp only [Finsupp.linearCombination, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe,
    id_eq, smul_eq_mul, add_left_inj]

Premises used: LinearMap.id_coe, add_left_inj, Finsupp.coe_lsum, LinearMap.coe_smulRight, smul_eq_mul, Finsupp.linearCombination, id_eq
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
q : MvPolynomial σ R :=
  (g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯)
h1 :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ Membership.mem (γ := Set (MvPolynomial σ R)) {b} b

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
q : MvPolynomial σ R :=
  (g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯)
h1 :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ Eq (α := MvPolynomial σ R)
      ((g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
          (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯) :
        MvPolynomial σ R)
      (0 : MvPolynomial σ R) →
    0 *
        (↑(Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯) :
          MvPolynomial σ R) =
      0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
q : MvPolynomial σ R :=
  (g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯)
h1 :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
rw :
  ∀ (b_1 : (↑{b} : Type (max u_1 u_2))),
    Ne (α := MvPolynomial σ R) ((g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R) b_1 : MvPolynomial σ R)
        (0 : MvPolynomial σ R) →
      b_1 ≠ Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯ →
        HMul.hMul (α := MvPolynomial σ R)
            ((g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R) b_1 : MvPolynomial σ R)
            (↑b_1 : MvPolynomial σ R) =
          0
⊢ (g.sum fun (i : (↑{b} : Type (max u_1 u_2))) (c : MvPolynomial σ R) ↦ c * (↑i : MvPolynomial σ R)) = q * b

Tactic:
rw [Finsupp.sum_eq_single ⟨b, by simp⟩ _ (by simp)]

Premises used: Finsupp.sum_eq_single
-- Module: Mathlib.RingTheory.MvPolynomial.Groebner
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
g : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R
r : MvPolynomial σ R
hgr :
  f =
    HAdd.hAdd (α := MvPolynomial σ R)
      ((Finsupp.linearCombination (MvPolynomial σ R) fun (b_1 : (↑{b} : Type (max u_1 u_2))) ↦
              (↑b_1 : MvPolynomial σ R) :
            (a : (↑{b} : Type (max u_1 u_2)) →₀ MvPolynomial σ R) → MvPolynomial σ R)
          g :
        MvPolynomial σ R)
      r
q : MvPolynomial σ R :=
  (g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R)
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯)
h1 :
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (b * q)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
h2 : ∀ c ∈ r.support, ¬m.degree b ≤ c
⊢ ∀ (b_1 : (↑{b} : Type (max u_1 u_2))),
    Ne (α := MvPolynomial σ R) ((g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R) b_1 : MvPolynomial σ R)
        (0 : MvPolynomial σ R) →
      b_1 ≠ Subtype.mk (p := fun (x : MvPolynomial σ R) ↦ Membership.mem (γ := Set (MvPolynomial σ R)) {b} x) b ⋯ →
        HMul.hMul (α := MvPolynomial σ R)
            ((g : (a : (↑{b} : Type (max u_1 u_2))) → MvPolynomial σ R) b_1 : MvPolynomial σ R)
            (↑b_1 : MvPolynomial σ R) =
          0

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
rw :
  Eq (α := Multiset σ) (weightedTotalDegree (fun (i : σ) ↦ {i}) p)
    (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
⊢ weightedTotalDegree (fun (i : σ) ↦ {i}) p = p.degrees

Tactic:
rw [degrees_def]

Premises used: MvPolynomial.degrees_def
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
⊢ Eq (α := Multiset σ) (weightedTotalDegree (fun (i : σ) ↦ {i}) p)
    (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
⊢ weightedTotalDegree 1 φ = φ.totalDegree

Tactic:
simp only [totalDegree, weightedTotalDegree, weight, LinearMap.toAddMonoidHom_coe,
    linearCombination, Pi.one_apply, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe,
    id, smul_eq_mul, mul_one]

Premises used: LinearMap.toAddMonoidHom_coe, Finsupp.weight, LinearMap.id_coe, Pi.one_apply, MvPolynomial.weightedTotalDegree, id, Finsupp.coe_lsum, MvPolynomial.totalDegree, LinearMap.coe_smulRight, smul_eq_mul, mul_one, Finsupp.linearCombination
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
p : MvPolynomial σ R
simp :
  Eq (α := ℕ)
    (p.support.sup fun (s : σ →₀ ℕ) ↦
      (LinearMap.toAddMonoidHom (R := ℕ) (S := ℕ) (modM₁ := module σ ℕ) (modM₂ := AddCommMonoid.toNatModule) (σ :=
            RingHom.id ℕ)
            ((lsum ℕ : (a : σ → ℕ →ₗ[ℕ] ℕ) → (σ →₀ ℕ) →ₗ[ℕ] ℕ) fun (i_1 : σ) ↦
              LinearMap.smulRight LinearMap.id (if i_1 = i then 1 else 0)) :
          (a : σ →₀ ℕ) → ℕ)
        s)
    (p.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))
⊢ weightedTotalDegree (Pi.single (M := fun (a : σ) ↦ ℕ) i 1) p = degreeOf i p

Tactic:
simp only [weightedTotalDegree, weight, linearCombination, Pi.single_apply, degreeOf, degrees,
    Multiset.count_finset_sup]

Premises used: Finsupp.weight, Pi.single_apply, MvPolynomial.weightedTotalDegree, Multiset.count_finset_sup, Finsupp.linearCombination, MvPolynomial.degrees, MvPolynomial.degreeOf
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
p : MvPolynomial σ R
e_f :
  Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ)
    (fun (s : σ →₀ ℕ) ↦
      (LinearMap.toAddMonoidHom (R := ℕ) (S := ℕ) (modM₁ := module σ ℕ) (modM₂ := AddCommMonoid.toNatModule) (σ :=
            RingHom.id ℕ)
            ((lsum ℕ : (a : σ → ℕ →ₗ[ℕ] ℕ) → (σ →₀ ℕ) →ₗ[ℕ] ℕ) fun (i_1 : σ) ↦
              LinearMap.smulRight LinearMap.id (if i_1 = i then 1 else 0)) :
          (a : σ →₀ ℕ) → ℕ)
        s)
    fun (a : σ →₀ ℕ) ↦ Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a)
⊢ Eq (α := ℕ)
    (p.support.sup fun (s : σ →₀ ℕ) ↦
      (LinearMap.toAddMonoidHom (R := ℕ) (S := ℕ) (modM₁ := module σ ℕ) (modM₂ := AddCommMonoid.toNatModule) (σ :=
            RingHom.id ℕ)
            ((lsum ℕ : (a : σ → ℕ →ₗ[ℕ] ℕ) → (σ →₀ ℕ) →ₗ[ℕ] ℕ) fun (i_1 : σ) ↦
              LinearMap.smulRight LinearMap.id (if i_1 = i then 1 else 0)) :
          (a : σ →₀ ℕ) → ℕ)
        s)
    (p.support.sup fun (a : σ →₀ ℕ) ↦ Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a))

Tactic:
congr
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
p : MvPolynomial σ R
e_f :
  ∀ (d : σ →₀ ℕ),
    (LinearMap.toAddMonoidHom (R := ℕ) (S := ℕ) (modM₁ := module σ ℕ) (modM₂ := AddCommMonoid.toNatModule) (σ :=
            RingHom.id ℕ)
            ((lsum ℕ : (a : σ → ℕ →ₗ[ℕ] ℕ) → (σ →₀ ℕ) →ₗ[ℕ] ℕ) fun (i_1 : σ) ↦
              LinearMap.smulRight LinearMap.id (if i_1 = i then 1 else 0)) :
          (a : σ →₀ ℕ) → ℕ)
        d =
      Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) d)
⊢ Eq.{u_1 + 1} (α := (σ →₀ ℕ) → ℕ)
    (fun (s : σ →₀ ℕ) ↦
      (LinearMap.toAddMonoidHom (R := ℕ) (S := ℕ) (modM₁ := module σ ℕ) (modM₂ := AddCommMonoid.toNatModule) (σ :=
            RingHom.id ℕ)
            ((lsum ℕ : (a : σ → ℕ →ₗ[ℕ] ℕ) → (σ →₀ ℕ) →ₗ[ℕ] ℕ) fun (i_1 : σ) ↦
              LinearMap.smulRight LinearMap.id (if i_1 = i then 1 else 0)) :
          (a : σ →₀ ℕ) → ℕ)
        s)
    fun (a : σ →₀ ℕ) ↦ Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) a)

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
p : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (LinearMap.toAddMonoidHom (R := ℕ) (S := ℕ) (modM₁ := module σ ℕ) (modM₂ := AddCommMonoid.toNatModule) (σ :=
          RingHom.id ℕ)
          ((lsum ℕ : (a : σ → ℕ →ₗ[ℕ] ℕ) → (σ →₀ ℕ) →ₗ[ℕ] ℕ) fun (i_1 : σ) ↦
            LinearMap.smulRight LinearMap.id (if i_1 = i then 1 else 0)) :
        (a : σ →₀ ℕ) → ℕ)
      d =
    Multiset.count i ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) d)

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
rw :
  Eq (α := ℕ) (P.support.sup ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e))
    (P.support.sup fun (s : σ →₀ ℕ) ↦ (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s)
⊢ Eq (α := ℕ)
    (Finset.sup (support.{u_3, u_6} (R := R) ((rename e : (a : MvPolynomial σ R) → MvPolynomial τ R) P))
      fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s)
    (P.support.sup fun (s : σ →₀ ℕ) ↦ (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s)

Tactic:
rw [support_rename_of_injective he, Finset.sup_image]

Premises used: MvPolynomial.support_rename_of_injective, Finset.sup_image
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
e_f :
  Eq (α := (σ →₀ ℕ) → ℕ) ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) fun (s : σ →₀ ℕ) ↦
    (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s
⊢ Eq (α := ℕ) (P.support.sup ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e))
    (P.support.sup fun (s : σ →₀ ℕ) ↦ (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s)

Tactic:
congr
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
e_f :
  ∀ (x : σ →₀ ℕ),
    Eq (α := ℕ) (((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) x : ℕ)
      ((weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) x : ℕ)
⊢ Eq (α := (σ →₀ ℕ) → ℕ) ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) fun (s : σ →₀ ℕ) ↦
    (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
x : σ →₀ ℕ
⊢ Eq (α := ℕ)
    (((fun (s : τ →₀ ℕ) ↦
            (LinearMap.toAddMonoidHom (modM₂ := AddCommMonoid.toNatModule) (linearCombination ℕ w) : (a : τ →₀ ℕ) → ℕ)
              s) ∘
          mapDomain e)
        x :
      ℕ)
    ((LinearMap.toAddMonoidHom (modM₂ := AddCommMonoid.toNatModule) (linearCombination ℕ (w ∘ e)) : (a : σ →₀ ℕ) → ℕ)
        x :
      ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_3
inst : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
unfold :
  Eq (α := ℕ)
    (Finset.sup (support.{u_3, u_6} (R := R) ((rename e : (a : MvPolynomial σ R) → MvPolynomial τ R) P))
      fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s)
    (P.support.sup fun (s : σ →₀ ℕ) ↦ (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s)
unfold₁ :
  Eq (α := ℕ) (P.support.sup ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e))
    (P.support.sup fun (s : σ →₀ ℕ) ↦ (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s)
e_f e_f₁ :
  Eq (α := (σ →₀ ℕ) → ℕ) ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) fun (s : σ →₀ ℕ) ↦
    (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s
e_f₂ e_f₃ :
  ∀ (x : σ →₀ ℕ),
    Eq (α := ℕ) (((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) x : ℕ)
      ((weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) x : ℕ)
e_f₄ e_f₅ :
  ∀ (x : σ →₀ ℕ),
    Eq (α := ℕ)
      (((fun (s : τ →₀ ℕ) ↦
              (LinearMap.toAddMonoidHom (modM₂ := AddCommMonoid.toNatModule) (linearCombination ℕ w) : (a : τ →₀ ℕ) → ℕ)
                s) ∘
            mapDomain e)
          x :
        ℕ)
      ((LinearMap.toAddMonoidHom (modM₂ := AddCommMonoid.toNatModule) (linearCombination ℕ (w ∘ e)) : (a : σ →₀ ℕ) → ℕ)
          x :
        ℕ)
⊢ weightedTotalDegree.{u_3, 0, u_6} (R := R) w ((rename e : (a : MvPolynomial σ R) → MvPolynomial τ R) P) =
    weightedTotalDegree (w ∘ e) P

Tactic:
classical
  unfold weightedTotalDegree
  rw [support_rename_of_injective he, Finset.sup_image]
  congr; ext; unfold weight; simp

Premises used: Finsupp.weight, MvPolynomial.weightedTotalDegree, Finset.sup_image
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} b
c : σ →₀ ℕ
hc : coeff c (a + b) ≠ 0
⊢ coeff c a + coeff c b ≠ 0

Tactic:
rw [coeff_add] at hc

Premises used: MvPolynomial.coeff_add
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
contrapose! : ∀ (hc : coeff c a = 0 ∧ coeff c b = 0), coeff c a + coeff c b = 0
⊢ coeff c a ≠ 0 ∨ coeff c b ≠ 0

Tactic:
contrapose! hc
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} b
c : σ →₀ ℕ
hc : coeff c a = 0 ∧ coeff c b = 0
⊢ coeff c a + coeff c b = 0

Tactic:
simp only [hc, add_zero]

Premises used: add_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
inl : ∀ (h : coeff c a ≠ 0), (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n
inr : ∀ (h : coeff c b ≠ 0), (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n

Tactic:
obtain h | h : coeff c a ≠ 0 ∨ coeff c b ≠ 0 := by
      contrapose! hc
      simp only [hc, add_zero]

Premises used: MvPolynomial.coeff
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c a ≠ 0
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n

Tactic:
ha h
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c a ≠ 0
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n

Tactic:
exact ha h
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c b ≠ 0
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n

Tactic:
hb h
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c b ≠ 0
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n

Tactic:
exact hb h
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
c : σ →₀ ℕ
hc : coeff c (r • a) ≠ 0
⊢ r • coeff c a ≠ 0

Tactic:
rw [coeff_smul] at hc

Premises used: MvPolynomial.coeff_smul
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
n : ℕ
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | x.IsHomogeneous n} a
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
a₁ : coeff c a ≠ 0
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n

Tactic:
apply ha