awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (coeff c ((monomial d : (a : R) → MvPolynomial σ R) r)) 0
⊢ (if d = c then r else 0) ≠ 0

Tactic:
rw [coeff_monomial] at hc

Premises used: MvPolynomial.coeff_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
c : σ →₀ ℕ
hc : (if d = c then r else 0) ≠ 0
pos : ∀ (h : d = c) (hc : r ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
neg : ∀ (h : ¬d = c) (hc : Ne.{u_1 + 1} (α := R) 0 0), (weight w : (a : σ →₀ ℕ) → M) c = m
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m

Tactic:
split_ifs at hc with h
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
c : σ →₀ ℕ
h : d = c
hc : r ≠ 0
pos : (weight w : (a : σ →₀ ℕ) → M) d = m
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m

Tactic:
subst c
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
hc : r ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) d = m

Tactic:
hm
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
hc : r ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) d = m

Tactic:
exact hm
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
c : σ →₀ ℕ
h : ¬d = c
hc : Ne.{u_1 + 1} (α := R) 0 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m

Tactic:
contradiction
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : (weight w : (a : σ →₀ ℕ) → M) d = m
intro intro₁ :
  ∀ ⦃c : σ →₀ ℕ⦄ (hc : Ne.{u_1 + 1} (α := R) (coeff c ((monomial d : (a : R) → MvPolynomial σ R) r)) 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m
intro₂ : ∀ ⦃c : σ →₀ ℕ⦄ (hc : (if d = c then r else 0) ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
pos : ∀ ⦃c : σ →₀ ℕ⦄ (h : d = c) (hc : r ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m
neg neg₁ : ∀ ⦃c : σ →₀ ℕ⦄ (h : ¬d = c) (hc : Ne.{u_1 + 1} (α := R) 0 0), (weight w : (a : σ →₀ ℕ) → M) c = m
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w ((monomial d : (a : R) → MvPolynomial σ R) r) m

Tactic:
classical
  intro c hc
  rw [coeff_monomial] at hc
  split_ifs at hc with h
  · subst c
    exact hm
  · contradiction

Premises used: MvPolynomial.coeff_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
⊢ weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)

Tactic:
have h := weightedTotalDegree_coe w p (MvPolynomial.ne_zero_iff.mpr ⟨d, hd⟩)
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h : weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)
⊢ Eq.{u_2 + 1} (α := WithBot M) (p.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M))
    (↑⊥ : WithBot M)

Tactic:
simp only [weightedTotalDegree', hp] at h

Premises used: MvPolynomial.weightedTotalDegree'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h :
  Eq.{u_2 + 1} (α := WithBot M) (p.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M))
    (↑⊥ : WithBot M)
rw :
  LE.le.{u_2} (α := WithBot M) ((↑((weight w : (a : σ →₀ ℕ) → M) d) : WithBot M) : WithBot M)
    (p.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) : WithBot M)
⊢ Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) (⊥ : M)

Tactic:
rw [eq_bot_iff, ← WithBot.coe_le_coe, ← h]

Premises used: WithBot.coe_le_coe, eq_bot_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h :
  Eq.{u_2 + 1} (α := WithBot M) (p.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M))
    (↑⊥ : WithBot M)
⊢ LE.le.{u_2} (α := WithBot M) ((↑((weight w : (a : σ →₀ ℕ) → M) d) : WithBot M) : WithBot M)
    (p.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) : WithBot M)

Tactic:
apply Finset.le_sup (mem_support_iff.mpr hd)

Premises used: Iff.mpr, MvPolynomial.mem_support_iff, Finset.le_sup
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
r : R
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w ((C : (a : R) → MvPolynomial σ R) r) 0

Tactic:
isWeightedHomogeneous_monomial _ _ _ (map_zero _)

Premises used: map_zero, MvPolynomial.isWeightedHomogeneous_monomial, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w 0 m

Tactic:
(weightedHomogeneousSubmodule R w m).zero_mem

Premises used: MvPolynomial.weightedHomogeneousSubmodule, Set.Mem, setOf, Submodule.zero_mem, MvPolynomial.IsWeightedHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w 1 0

Tactic:
isWeightedHomogeneous_C _ _

Premises used: MvPolynomial.isWeightedHomogeneous_C, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
i : σ
hm : (weight w : (a : σ →₀ ℕ) → M) (Finsupp.single i 1) = w i
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (X i) (w i)

Tactic:
apply isWeightedHomogeneous_monomial

Premises used: MvPolynomial.isWeightedHomogeneous_monomial
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
i : σ
⊢ (weight w : (a : σ →₀ ℕ) → M) (Finsupp.single i 1) = w i

Tactic:
simp only [weight, LinearMap.toAddMonoidHom_coe, linearCombination_single, one_nsmul]

Premises used: LinearMap.toAddMonoidHom_coe, Finsupp.weight, Finsupp.linearCombination_single, one_nsmul
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n
⊢ ¬coeff d φ ≠ 0

Tactic:
have aux := mt (@hφ d) hd
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : (weight w : (a : σ →₀ ℕ) → M) d ≠ n
aux : ¬coeff d φ ≠ 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (aux : coeff d φ = 0), coeff d φ = 0
⊢ coeff d φ = 0

Tactic:
rwa [Classical.not_not] at aux

Premises used: Classical.not_not
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
⊢ ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0

Tactic:
exists_coeff_ne_zero hφ

Premises used: MvPolynomial.exists_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
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.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
rw : (weight w : (a : σ →₀ ℕ) → M) d = n
rw₁ rw₂ : Eq.{u_2 + 1} (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) d : M)
⊢ m = n

Tactic:
rw [← hm hd, ← hn hd]
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ ψ : MvPolynomial σ R
n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
hψ : IsWeightedHomogeneous w ψ n
⊢ IsWeightedHomogeneous w (φ + ψ) n

Tactic:
(weightedHomogeneousSubmodule R w n).add_mem hφ hψ

Premises used: MvPolynomial.weightedHomogeneousSubmodule, Set.Mem, setOf, MvPolynomial.IsWeightedHomogeneous, Submodule.add_mem
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : M
w : σ → M
h : ∀ i ∈ s, IsWeightedHomogeneous w (φ i) n
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∑ i ∈ s, φ i) n

Tactic:
(weightedHomogeneousSubmodule R w n).sum_mem h

Premises used: MvPolynomial.weightedHomogeneousSubmodule, Set.Mem, setOf, Submodule.sum_mem, MvPolynomial.IsWeightedHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ ψ : MvPolynomial σ R
m n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
hψ : IsWeightedHomogeneous w ψ n
⊢ IsWeightedHomogeneous w (φ * ψ) (m + n)

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

Premises used: MvPolynomial.weightedHomogeneousSubmodule_mul, Submodule.mul_mem_mul, Set.Mem, setOf, MvPolynomial.IsWeightedHomogeneous
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
r : R
rw :
  IsWeightedHomogeneous w (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ)
    (0 + m)
⊢ IsWeightedHomogeneous w (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ)
    m

Tactic:
rw [← zero_add m]

Premises used: zero_add
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
r : R
⊢ IsWeightedHomogeneous w (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ)
    (0 + m)

Tactic:
(isWeightedHomogeneous_C w r).mul hφ

Premises used: MvPolynomial.IsWeightedHomogeneous.mul, MvPolynomial.isWeightedHomogeneous_C
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
r : R
⊢ IsWeightedHomogeneous w (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) φ)
    (0 + m)

Tactic:
exact (isWeightedHomogeneous_C w r).mul hφ

Premises used: MvPolynomial.IsWeightedHomogeneous.mul, MvPolynomial.isWeightedHomogeneous_C
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
zero : IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w 1 0
⊢ IsWeightedHomogeneous w (HPow.hPow (β := ℕ) φ 0) (HSMul.hSMul (α := ℕ) 0 m)

Tactic:
rw [pow_zero, zero_smul]

Premises used: pow_zero, zero_smul
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w 1 0

Tactic:
isWeightedHomogeneous_one R w

Premises used: MvPolynomial.isWeightedHomogeneous_one
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w 1 0

Tactic:
exact isWeightedHomogeneous_one R w

Premises used: MvPolynomial.isWeightedHomogeneous_one
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
ih : IsWeightedHomogeneous w (φ ^ n) (n • m)
succ : IsWeightedHomogeneous w (φ ^ n * φ) (n • m + m)
⊢ IsWeightedHomogeneous w (φ ^ (n + 1)) ((n + 1) • m)

Tactic:
rw [pow_succ, succ_nsmul]

Premises used: pow_succ, succ_nsmul
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
ih : IsWeightedHomogeneous w (φ ^ n) (n • m)
⊢ IsWeightedHomogeneous w (φ ^ n * φ) (n • m + m)

Tactic:
ih.mul hφ

Premises used: MvPolynomial.IsWeightedHomogeneous.mul
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
ih : IsWeightedHomogeneous w (φ ^ n) (n • m)
⊢ IsWeightedHomogeneous w (φ ^ n * φ) (n • m + m)

Tactic:
exact ih.mul hφ

Premises used: MvPolynomial.IsWeightedHomogeneous.mul
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
zero : IsWeightedHomogeneous w (HPow.hPow (β := ℕ) φ 0) (HSMul.hSMul (α := ℕ) 0 m)
succ : ∀ (n : ℕ) (ih : IsWeightedHomogeneous w (φ ^ n) (n • m)), IsWeightedHomogeneous w (φ ^ (n + 1)) ((n + 1) • m)
⊢ IsWeightedHomogeneous w (φ ^ n) (n • m)

Tactic:
induction n with
  | zero => rw [pow_zero, zero_smul]; exact isWeightedHomogeneous_one R w
  | succ n ih => rw [pow_succ, succ_nsmul]; exact ih.mul hφ

Premises used: pow_succ, MvPolynomial.isWeightedHomogeneous_one, pow_zero, zero_smul, AddMonoidAlgebra.zero, succ_nsmul
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
⊢ (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
refine_1 :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
refine_2 :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)
⊢ (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)

Tactic:
refine Finset.induction_on s ?_ ?_
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsWeightedHomogeneous w (φ i) (n i)
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)

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

Premises used: Finset.prod_empty, MvPolynomial.isWeightedHomogeneous_one, Finset.sum_empty
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH :
  (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
refine_2 : IsWeightedHomogeneous w (φ i * ∏ i ∈ s, φ i) (n i + ∑ i ∈ s, n i)
⊢ IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ 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.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH :
  (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
apply : ∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)
⊢ IsWeightedHomogeneous w (φ i * ∏ i ∈ s, φ i) (n i + ∑ i ∈ s, n i)

Tactic:
apply (h i (Finset.mem_insert_self _ _)).mul (IH _)

Premises used: Finset.mem_insert_self, MvPolynomial.IsWeightedHomogeneous.mul
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH :
  (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsWeightedHomogeneous w (φ j) (n j)

Tactic:
h j (Finset.mem_insert_of_mem hjs)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s_1 : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
i : ι
s : Finset ι
his : i ∉ s
IH :
  (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
h : ∀ i_1 ∈ insert i s, IsWeightedHomogeneous w (φ i_1) (n i_1)
j : ι
hjs : j ∈ s
⊢ IsWeightedHomogeneous w (φ j) (n j)

Tactic:
exact h j (Finset.mem_insert_of_mem hjs)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
ι : Type u_4
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → M
w : σ → M
refine_1 :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ ∅, φ i) (∑ i ∈ ∅, n i)
refine_2 refine_2₁ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, IsWeightedHomogeneous w (φ i) (n i)) →
          IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ insert a s, φ i) (∑ i ∈ insert a s, n i)
⊢ (∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) →
    IsWeightedHomogeneous.{u_1, u_2, u_3} (R := R) w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)

Tactic:
classical
  refine Finset.induction_on s ?_ ?_
  · intro
    simp only [isWeightedHomogeneous_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 (Finset.mem_insert_self _ _)).mul (IH _)
    intro j hjs
    exact h j (Finset.mem_insert_of_mem hjs)

Premises used: Finset.prod_empty, Finset.prod_insert, MvPolynomial.isWeightedHomogeneous_one, Finset.sum_empty, Finset.sum_insert, not_false_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
a : (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)) ≤ (↑n : WithBot M)
a₁ : (↑n : WithBot M) ≤ φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)
⊢ (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)) = (↑n : WithBot M)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
a : ∀ (b : σ →₀ ℕ), coeff b φ ≠ 0 → (weight w : (a : σ →₀ ℕ) → M) b ≤ n
⊢ (φ.support.sup fun (s : σ →₀ ℕ) ↦ (↑((weight w : (a : σ →₀ ℕ) → M) s) : WithBot M)) ≤ (↑n : WithBot M)

Tactic:
simp only [Finset.sup_le_iff, mem_support_iff, WithBot.coe_le_coe]

Premises used: MvPolynomial.mem_support_iff, WithBot.coe_le_coe, Finset.sup_le_iff
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
⊢ ∀ (b : σ →₀ ℕ), coeff b φ ≠ 0 → (weight w : (a : σ →₀ ℕ) → M) b ≤ n

Tactic:
fun d hd => le_of_eq (hφ hd)

Premises used: le_of_eq
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
φ : MvPolynomial σ R
n : M
inst_2 : SemilatticeSup M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
h : φ ≠ 0
⊢ ∀ (b : σ →₀ ℕ), coeff b φ ≠ 0 → (weight w : (a : σ →₀ ℕ) → M) b ≤ n

Tactic:
exact fun d hd => le_of_eq (hφ hd)

Premises used: le_of_eq