awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ f = q * b + r
have 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
Tactic: rw [hgr]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ 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
have simp : (g.sum fun (i : (↑{b} : Type (max u_1 u_2))) (c : MvPolynomial σ R) ↦ c * (↑i : MvPolynomial σ R)) = q * b
Tactic: simp only [Finsupp.linearCombination, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe,
    id_eq, smul_eq_mul, add_left_inj]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Groebner (goal)
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
⊢ (g.sum fun (i : (↑{b} : Type (max u_1 u_2))) (c : MvPolynomial σ R) ↦ c * (↑i : MvPolynomial σ R)) = q * b
have 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 sorry →
      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: rw [Finsupp.sum_eq_single ⟨b, by simp⟩ _ (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
p : MvPolynomial σ R
⊢ weightedTotalDegree (fun (i : σ) ↦ {i}) p = p.degrees
have rw : Eq (α := Multiset σ) (weightedTotalDegree (fun (i : σ) ↦ {i}) p)
  (p.support.sup fun (s : σ →₀ ℕ) ↦ (toMultiset : (a : σ →₀ ℕ) → Multiset σ) s)
Tactic: rw [degrees_def]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
p : MvPolynomial σ R
⊢ weightedTotalDegree (Pi.single (M := fun (a : σ) ↦ ℕ) i 1) p = degreeOf i p
have 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))
Tactic: simp only [weightedTotalDegree, weight, linearCombination, Pi.single_apply, degreeOf, degrees,
    Multiset.count_finset_sup]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
p : MvPolynomial σ R
⊢ 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))
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
i : σ
p : MvPolynomial σ R
⊢ 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)
have 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)
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
R : Type u_3
inst : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
⊢ 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)
have rw : Eq (α := ℕ) (P.support.sup ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e))
  (P.support.sup fun (s : σ →₀ ℕ) ↦ (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s)
Tactic: rw [support_rename_of_injective he, Finset.sup_image]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
R : Type u_3
inst : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
⊢ Eq (α := ℕ) (P.support.sup ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e))
    (P.support.sup fun (s : σ →₀ ℕ) ↦ (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s)
have e_f : Eq (α := (σ →₀ ℕ) → ℕ) ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) fun (s : σ →₀ ℕ) ↦
  (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
R : Type u_3
inst : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
⊢ Eq (α := (σ →₀ ℕ) → ℕ) ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) fun (s : σ →₀ ℕ) ↦
    (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s
have e_f : ∀ (x : σ →₀ ℕ),
  Eq (α := ℕ) (((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) x : ℕ)
    ((weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) x : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
R : Type u_3
inst : CommSemiring R
σ : Type u_5
τ : Type u_6
e : σ → τ
w : τ → ℕ
P : MvPolynomial σ R
he : Function.Injective e
⊢ weightedTotalDegree.{u_3, 0, u_6} (R := R) w ((rename e : (a : MvPolynomial σ R) → MvPolynomial τ R) P) =
    weightedTotalDegree (w ∘ e) P
have 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)
Tactic: classical
  unfold weightedTotalDegree
  rw [support_rename_of_injective he, Finset.sup_image]
  congr; ext; unfold weight; simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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)
⊢ weightedTotalDegree.{u_3, 0, u_6} (R := R) w ((rename e : (a : MvPolynomial σ R) → MvPolynomial τ R) P) =
    weightedTotalDegree (w ∘ e) P
have unfold₁ : Eq (α := ℕ) (P.support.sup ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e))
  (P.support.sup fun (s : σ →₀ ℕ) ↦ (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s)
Tactic: classical
  unfold weightedTotalDegree
  rw [support_rename_of_injective he, Finset.sup_image]
  congr; ext; unfold weight; simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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)
⊢ weightedTotalDegree.{u_3, 0, u_6} (R := R) w ((rename e : (a : MvPolynomial σ R) → MvPolynomial τ R) P) =
    weightedTotalDegree (w ∘ e) P
have e_f : Eq (α := (σ →₀ ℕ) → ℕ) ((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) fun (s : σ →₀ ℕ) ↦
  (weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) s
Tactic: classical
  unfold weightedTotalDegree
  rw [support_rename_of_injective he, Finset.sup_image]
  congr; ext; unfold weight; simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ weightedTotalDegree.{u_3, 0, u_6} (R := R) w ((rename e : (a : MvPolynomial σ R) → MvPolynomial τ R) P) =
    weightedTotalDegree (w ∘ e) P
have e_f₂ : ∀ (x : σ →₀ ℕ),
  Eq (α := ℕ) (((fun (s : τ →₀ ℕ) ↦ (weight w : (a : τ →₀ ℕ) → ℕ) s) ∘ mapDomain e) x : ℕ)
    ((weight (w ∘ e) : (a : σ →₀ ℕ) → ℕ) x : ℕ)
Tactic: classical
  unfold weightedTotalDegree
  rw [support_rename_of_injective he, Finset.sup_image]
  congr; ext; unfold weight; simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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 : ℕ)
⊢ weightedTotalDegree.{u_3, 0, u_6} (R := R) w ((rename e : (a : MvPolynomial σ R) → MvPolynomial τ R) P) =
    weightedTotalDegree (w ∘ e) P
have 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 :
      ℕ)
Tactic: classical
  unfold weightedTotalDegree
  rw [support_rename_of_injective he, Finset.sup_image]
  congr; ext; unfold weight; simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n
have hc₁ : coeff c a + coeff c b ≠ 0
Tactic: rw [coeff_add] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ coeff c a ≠ 0 ∨ coeff c b ≠ 0
have contrapose! : ∀ (hc : coeff c a = 0 ∧ coeff c b = 0), coeff c a + coeff c b = 0
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n
have inl : ∀ (h : coeff c a ≠ 0), (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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n
have inr : ∀ (h : coeff c b ≠ 0), (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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (hypothesis)
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
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n
have hc₁ : r • coeff c a ≠ 0
Tactic: rw [coeff_smul] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
⊢ (weight 1 : (a : σ →₀ ℕ) → ℕ) c = n
have a₁ : coeff c a ≠ 0
Tactic: apply ha
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
h : coeff c a = 0
⊢ False
have a₁ : r • coeff c a = 0
Tactic: apply hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
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
h : coeff c a = 0
⊢ r • coeff c a = 0
have a₁ : HSMul.hSMul (β := R) r 0 = 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n)
    (supported R R {d : σ →₀ ℕ | (degree : (a : σ →₀ ℕ) → ℕ) d = n})
have simp_rw : Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R n)
  (supported R R {d : σ →₀ ℕ | (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n})
Tactic: simp_rw [degree_eq_weight_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) (Submodule.span R (Set.range X))
have rw : Eq (α := Submodule R (MvPolynomial σ R))
  (Submodule.span R
    ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
  (Submodule.span R (Set.range X))
Tactic: rw [MvPolynomial.homogeneousSubmodule_eq_finsupp_supported, Finsupp.supported_eq_span_single]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
    (Submodule.span R (Set.range X))
have simp_rw : Eq (α := Submodule R (MvPolynomial σ R))
  (Submodule.span R
    ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) ''
      {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
  (Submodule.span R (Set.range X))
Tactic: simp_rw [MvPolynomial.single_eq_monomial, ← Finsupp.range_single_one, ← Set.range_comp,
    Function.comp_def, ← X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
simp_rw :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) ''
        {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
    (Submodule.span R (Set.range X))
⊢ Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
    (Submodule.span R (Set.range X))
have simp_rw₁ : Eq (α := Submodule R (MvPolynomial σ R))
  (Submodule.span R
    ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) '' Set.range fun (a : σ) ↦ single a 1))
  (Submodule.span R (Set.range X))
Tactic: simp_rw [MvPolynomial.single_eq_monomial, ← Finsupp.range_single_one, ← Set.range_comp,
    Function.comp_def, ← X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Homogeneous (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
simp_rw :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) ''
        {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
    (Submodule.span R (Set.range X))
simp_rw₁ :
  Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) '' Set.range fun (a : σ) ↦ single a 1))
    (Submodule.span R (Set.range X))
⊢ Eq (α := Submodule R (MvPolynomial σ R))
    (Submodule.span R
      ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (1 : ℕ)}))
    (Submodule.span R (Set.range X))
have simp_rw₂ : Eq (α := Submodule R (MvPolynomial σ R))
  (Submodule.span R
    (Set.range (ι := σ) ((fun (a : σ →₀ ℕ) ↦ (monomial a : (a : R) → MvPolynomial σ R) 1) ∘ fun (a : σ) ↦ single a 1)))
  (Submodule.span R (Set.range X))
Tactic: simp_rw [MvPolynomial.single_eq_monomial, ← Finsupp.range_single_one, ← Set.range_comp,
    Function.comp_def, ← X_pow_eq_monomial, pow_one]