awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
n : ℕ
x : MvPolynomial σ R
hx : x.IsHomogeneous n
refine_2 : 0 ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
refine_2₁ :
  ∀ (p q : MvPolynomial σ R),
    IsWeightedHomogeneous 1 p n →
      IsWeightedHomogeneous 1 q n →
        ∀ (hp : p ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n)
          (hq : q ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n),
          p + q ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n
refine_2₂ :
  ∀ (d : σ →₀ ℕ) (r : R) (hr : (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n),
    Membership.mem (α := MvPolynomial σ R)
      (HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n)
      ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
⊢ x ∈ HPow.hPow (α := Submodule R (MvPolynomial σ R)) (homogeneousSubmodule σ R 1) n

Tactic:
induction hx using IsWeightedHomogeneous.induction_on with
    | zero => simp
    | add p q _ _ hp hq => exact Submodule.add_mem _ hp hq
    | monomial d r hr =>
      convert! monomial_mem_homogeneousSubmodule_pow_degree _ _
      rw [Finsupp.degree_eq_weight_one, ← Pi.one_def, ← hr]

Premises used: MvPolynomial.IsWeightedHomogeneous.induction_on, MvPolynomial.monomial, Finsupp.degree_eq_weight_one, MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, Pi.one_def
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : (degree : (a : σ →₀ ℕ) → ℕ) d ≠ n
⊢ (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ n

Tactic:
rw [degree_eq_weight_one] at hd

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ n
⊢ coeff d φ = 0

Tactic:
IsWeightedHomogeneous.coeff_eq_zero hφ d hd

Premises used: MvPolynomial.IsWeightedHomogeneous.coeff_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d ≠ n
⊢ coeff d φ = 0

Tactic:
exact IsWeightedHomogeneous.coeff_eq_zero hφ d hd

Premises used: MvPolynomial.IsWeightedHomogeneous.coeff_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
⊢ ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0

Tactic:
exists_coeff_ne_zero hφ

Premises used: MvPolynomial.exists_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
obtain : ∀ (d : σ →₀ ℕ) (hd : coeff d φ ≠ 0), m = n
⊢ m = n

Tactic:
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ

Premises used: MvPolynomial.exists_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
rw : (weight 1 : (a : σ →₀ ℕ) → ℕ) d = n
rw₁ rw₂ : Eq (α := ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ) ((weight 1 : (a : σ →₀ ℕ) → ℕ) d : ℕ)
⊢ m = n

Tactic:
rw [← hm hd, ← hn hd]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ ψ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
hψ : ψ.IsHomogeneous n
⊢ (φ + ψ).IsHomogeneous n

Tactic:
(homogeneousSubmodule σ R n).add_mem hφ hψ

Premises used: Set.Mem, MvPolynomial.homogeneousSubmodule, setOf, MvPolynomial.IsWeightedHomogeneous, MvPolynomial.IsHomogeneous, Submodule.add_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ℕ
h : ∀ i ∈ s, (φ i).IsHomogeneous n
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∑ i ∈ s, φ i) n

Tactic:
(homogeneousSubmodule σ R n).sum_mem h

Premises used: Set.Mem, MvPolynomial.homogeneousSubmodule, setOf, Submodule.sum_mem, MvPolynomial.IsWeightedHomogeneous, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
hψ : ψ.IsHomogeneous n
⊢ (φ * ψ).IsHomogeneous (m + n)

Tactic:
homogeneousSubmodule_mul m n <| Submodule.mul_mem_mul hφ hψ

Premises used: Submodule.mul_mem_mul, Set.Mem, setOf, MvPolynomial.IsWeightedHomogeneous, MvPolynomial.homogeneousSubmodule_mul, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)
revert :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)

Tactic:
revert h
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
refine_1 :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (φ i).IsHomogeneous (n i)),
    IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
refine_2 :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)),
          IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
        ∀ (h : ∀ i ∈ insert a s, (φ i).IsHomogeneous (n i)),
          IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)
⊢ ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)

Tactic:
refine Finset.induction_on s ?_ ?_
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (φ i).IsHomogeneous (n i)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)

Tactic:
simp only [isHomogeneous_one, Finset.sum_empty, Finset.prod_empty]

Premises used: Finset.prod_empty, MvPolynomial.isHomogeneous_one, Finset.sum_empty
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)
refine_2 : (φ i * ∏ i ∈ s, φ i).IsHomogeneous (n i + ∑ i ∈ s, n i)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ insert i s, φ i) (∑ i ∈ insert i s, n i)

Tactic:
simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]

Premises used: Finset.prod_insert, Finset.sum_insert, not_false_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)
⊢ i ∈ insert i s

Tactic:
grind
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)
apply : ∀ i ∈ s, (φ i).IsHomogeneous (n i)
⊢ (φ i * ∏ i ∈ s, φ i).IsHomogeneous (n i + ∑ i ∈ s, n i)

Tactic:
apply (h i (by grind)).mul (IH _)

Premises used: MvPolynomial.IsHomogeneous.mul
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
i : ι
s : Finset ι
his : i ∉ s
IH :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, (φ i_1).IsHomogeneous (n i_1)
⊢ ∀ i ∈ s, (φ i).IsHomogeneous (n i)

Tactic:
grind
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)
revert :
  ∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)), IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
refine_1 :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (φ i).IsHomogeneous (n i)),
    IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
refine_2 refine_2₁ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (∀ (h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)),
          IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
        ∀ (h : ∀ i ∈ insert a s, (φ i).IsHomogeneous (n i)),
          IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, φ i) (∑ i ∈ s, n i)

Tactic:
classical
  revert h
  refine Finset.induction_on s ?_ ?_
  · intro
    simp only [isHomogeneous_one, Finset.sum_empty, Finset.prod_empty]
  · intro i s his IH h
    simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
    apply (h i (by grind)).mul (IH _)
    grind

Premises used: Finset.prod_empty, Finset.prod_insert, MvPolynomial.isHomogeneous_one, Finset.sum_empty, Finset.sum_insert, not_false_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
r : R
⊢ (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ).IsHomogeneous m

Tactic:
simpa only [zero_add] using (isHomogeneous_C _ _).mul hφ

Premises used: zero_add, MvPolynomial.IsHomogeneous.mul, MvPolynomial.isHomogeneous_C
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
i : σ
⊢ (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
        (X i)).IsHomogeneous
    1

Tactic:
(isHomogeneous_X _ _).C_mul _

Premises used: MvPolynomial.isHomogeneous_X, MvPolynomial.IsHomogeneous.C_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ φ ^ n = ∏ _i ∈ Finset.range n, φ

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
rw : IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ _i ∈ Finset.range n, φ) (m * n)
⊢ (φ ^ n).IsHomogeneous (m * n)

Tactic:
rw [show φ ^ n = ∏ _i ∈ Finset.range n, φ by simp]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ m * n = ∑ _i ∈ Finset.range n, m

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
rw : IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ _i ∈ Finset.range n, φ) (∑ _i ∈ Finset.range n, m)
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ _i ∈ Finset.range n, φ) (m * n)

Tactic:
rw [show m * n = ∑ _i ∈ Finset.range n, m by simp [mul_comm]]
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ IsHomogeneous.{u_1, u_3} (σ := σ) (R := R) (∏ _i ∈ Finset.range n, φ) (∑ _i ∈ Finset.range n, m)

Tactic:
apply IsHomogeneous.prod _ _ _ (fun _ _ ↦ hφ)

Premises used: MvPolynomial.IsHomogeneous.prod
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
i : σ
n : ℕ
⊢ (HPow.hPow (α := MvPolynomial σ R) (X i) n).IsHomogeneous n

Tactic:
simpa only [one_mul] using (isHomogeneous_X _ _).pow n

Premises used: MvPolynomial.IsHomogeneous.pow, MvPolynomial.isHomogeneous_X, one_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
r : R
i : σ
n : ℕ
⊢ (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
        (HPow.hPow (α := MvPolynomial σ R) (X i) n)).IsHomogeneous
    n

Tactic:
(isHomogeneous_X_pow _ _).C_mul _

Premises used: MvPolynomial.IsHomogeneous.C_mul, MvPolynomial.isHomogeneous_X_pow
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
h :
  ∀ i ∈ (AddMonoidAlgebra.coeff φ).support,
    IsHomogeneous.{u_2, u_4} (σ := τ) (R := S)
      ((fun (s : σ →₀ ℕ) (a : R) ↦
          HMul.hMul (α := MvPolynomial τ S) (β := MvPolynomial τ S)
            ((f : (a : R) → MvPolynomial τ S) a : MvPolynomial τ S)
            (s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : MvPolynomial τ S))
        i ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i))
      (n * m)
⊢ (MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)

Tactic:
apply IsHomogeneous.sum

Premises used: MvPolynomial.IsHomogeneous.sum
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ (AddMonoidAlgebra.coeff φ).support
h :
  IsHomogeneous.{u_2, u_4} (σ := τ) (R := S)
    ((fun (s : σ →₀ ℕ) (a : R) ↦
        HMul.hMul (α := MvPolynomial τ S) (β := MvPolynomial τ S)
          ((f : (a : R) → MvPolynomial τ S) a : MvPolynomial τ S)
          (s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : MvPolynomial τ S))
      i ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i))
    (0 + n * m)
⊢ IsHomogeneous.{u_2, u_4} (σ := τ) (R := S)
    ((fun (s : σ →₀ ℕ) (a : R) ↦
        HMul.hMul (α := MvPolynomial τ S) (β := MvPolynomial τ S)
          ((f : (a : R) → MvPolynomial τ S) a : MvPolynomial τ S)
          (s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : MvPolynomial τ S))
      i ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i))
    (n * m)

Tactic:
rw [← zero_add (n * m)]

Premises used: HMul.hMul, zero_add
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ (AddMonoidAlgebra.coeff φ).support
⊢ IsHomogeneous.{u_2, u_4} (σ := τ) (R := S)
    (∏ i_1 ∈ i.support, (fun (n : σ) (e : ℕ) ↦ g n ^ e) i_1 ((i : (a : σ) → ℕ) i_1))
    (∑ i_1 ∈ i.support, HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) i_1 : ℕ))

Tactic:
IsHomogeneous.prod _ _ (fun k ↦ n * i k) _

Premises used: HMul.hMul, MvPolynomial.IsHomogeneous.prod, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ (AddMonoidAlgebra.coeff φ).support
h : n * m = ∑ i_1 ∈ i.support, HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) i_1 : ℕ)
convert_6 :
  ∀ i_1 ∈ i.support,
    IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((fun (n : σ) (e : ℕ) ↦ g n ^ e) i_1 ((i : (a : σ) → ℕ) i_1))
      ((fun (k : σ) ↦ HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) k : ℕ)) i_1)
⊢ IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) (i.prod fun (n : σ) (e : ℕ) ↦ g n ^ e) (n * m)

Tactic:
convert! IsHomogeneous.prod _ _ (fun k ↦ n * i k) _

Premises used: HMul.hMul, MvPolynomial.IsHomogeneous.prod, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ (AddMonoidAlgebra.coeff φ).support
⊢ Ne.{u_3 + 1} (α := R) ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i : R) (0 : R)

Tactic:
rw [Finsupp.mem_support_iff] at hi

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : Ne.{u_3 + 1} (α := R) ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i : R) (0 : R)
h : (n * i.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i)) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
⊢ n * m = ∑ i_1 ∈ i.support, HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) i_1 : ℕ)

Tactic:
rw [← Finset.mul_sum, ← hφ hi, weight_apply]

Premises used: Finset.mul_sum, Finsupp.weight_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : Ne.{u_3 + 1} (α := R) ((AddMonoidAlgebra.coeff φ : (a : σ →₀ ℕ) → R) i : R) (0 : R)
h : (n * i.sum fun (i : σ) (c : ℕ) ↦ c * 1 i) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
h₁ :
  n * ∑ x ∈ i.support, HMul.hMul (α := ℕ) (β := ℕ) ((i : (a : σ) → ℕ) x : ℕ) (1 x : ℕ) =
    n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
h₂ :
  n * ∑ x ∈ i.support, HMul.hMul (α := ℕ) (β := ℕ) ((i : (a : σ) → ℕ) x : ℕ) (1 : ℕ) =
    n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1
⊢ (n * i.sum fun (i : σ) (c : ℕ) ↦ HSMul.hSMul (β := ℕ) c (1 i)) = n * ∑ i_1 ∈ i.support, (i : (a : σ) → ℕ) i_1

Tactic:
simp_rw [smul_eq_mul, Finsupp.sum, Pi.one_apply, mul_one]

Premises used: Pi.one_apply, Finsupp.sum, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((f : (a : R) → MvPolynomial τ S) r) 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ (AddMonoidAlgebra.coeff φ).support
k : σ
⊢ IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((fun (n : σ) (e : ℕ) ↦ g n ^ e) k ((i : (a : σ) → ℕ) k))
    ((fun (k : σ) ↦ HMul.hMul (β := ℕ) n ((i : (a : σ) → ℕ) k : ℕ)) k)

Tactic:
apply (hg k).pow

Premises used: MvPolynomial.IsHomogeneous.pow
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
f : R →+* S
rw :
  IsHomogeneous.{u_1, u_4} (σ := σ) (R := S)
    ((eval₂Hom (RingHom.comp C f) X : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) n
⊢ IsHomogeneous.{u_1, u_4} (σ := σ) (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) n

Tactic:
rw [map_eq_eval₂Hom_C_comp]

Premises used: MvPolynomial.map_eq_eval₂Hom_C_comp
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
f : R →+* S
⊢ IsHomogeneous.{u_1, u_4} (σ := σ) (R := S)
    ((eval₂Hom (RingHom.comp C f) X : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) n

Tactic:
simpa [one_mul] using hφ.eval₂ _ _ (fun r ↦ isHomogeneous_C _ (f r)) (isHomogeneous_X _)

Premises used: MvPolynomial.isHomogeneous_X, MvPolynomial.IsHomogeneous.eval₂, one_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
n : ℕ
f : R →+* S
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsHomogeneous.{u_1, u_4} (σ := σ) (R := S) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) φ) n
⊢ φ.IsHomogeneous n

Tactic:
fun u hu ↦ h (coeff_map f φ u ▸ map_zero f ▸ hf.ne hu)

Premises used: Function.Injective.ne, Eq.rec, map_zero, MvPolynomial.coeff_map, MvPolynomial.IsWeightedHomogeneous, Eq.symm, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
inst_2 : Algebra R S
hφ : φ.IsHomogeneous m
g : σ → MvPolynomial τ S
hg : ∀ (i : σ), (g i).IsHomogeneous n
⊢ IsHomogeneous.{u_2, u_4} (σ := τ) (R := S) ((MvPolynomial.aeval g : (a : MvPolynomial σ R) → MvPolynomial τ S) φ)
    (n * m)

Tactic:
hφ.eval₂ _ _ (fun _ ↦ isHomogeneous_C _ _) hg

Premises used: Multiset.sum, Multiset.foldr, Algebra.algebraMap, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.isHomogeneous_C, MvPolynomial.IsHomogeneous.eval₂, DFunLike.coe, Finset.sum
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
⊢ (-φ).IsHomogeneous n

Tactic:
(homogeneousSubmodule σ R n).neg_mem hφ

Premises used: Set.Mem, MvPolynomial.homogeneousSubmodule, setOf, Submodule.neg_mem, MvPolynomial.IsWeightedHomogeneous, MvPolynomial.IsHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
R : Type u_5
σ : Type u_6
inst : CommRing R
φ ψ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
hψ : ψ.IsHomogeneous n
⊢ (φ - ψ).IsHomogeneous n

Tactic:
(homogeneousSubmodule σ R n).sub_mem hφ hψ

Premises used: Set.Mem, MvPolynomial.homogeneousSubmodule, setOf, MvPolynomial.IsWeightedHomogeneous, MvPolynomial.IsHomogeneous, Submodule.sub_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Homogeneous
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
a : ∀ b ∈ φ.support, (b.sum fun (x : σ) (e : ℕ) ↦ e) ≤ n
⊢ φ.totalDegree ≤ n

Tactic:
apply Finset.sup_le

Premises used: Finset.sup_le