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
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : p ≠ 0
⊢ ∃ (a : M), (↑a : WithBot M) = weightedTotalDegree' w p

Tactic:
rw [Ne, ← weightedTotalDegree'_eq_bot_iff w p, ← Ne, WithBot.ne_bot_iff_exists] at hp

Premises used: WithBot.ne_bot_iff_exists, Ne, MvPolynomial.weightedTotalDegree'_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 : ∃ (a : M), (↑a : WithBot M) = weightedTotalDegree' w p
obtain :
  ∀ (m : M) (hm : (↑m : WithBot M) = weightedTotalDegree' w p),
    weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)
⊢ weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : WithBot M)

Tactic:
obtain ⟨m, hm⟩ := hp
-- 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
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
a : weightedTotalDegree' w p ≤ (↑(weightedTotalDegree w p) : WithBot M)
a₁ : (↑(weightedTotalDegree w p) : WithBot M) ≤ weightedTotalDegree' w p
⊢ weightedTotalDegree' w p = (↑(weightedTotalDegree w p) : 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
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
a :
  ∀ b ∈ p.support,
    LE.le.{u_2} (α := M) ((weight w : (a : σ →₀ ℕ) → M) b : M)
      (p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s : M)
⊢ weightedTotalDegree' w p ≤ (↑(weightedTotalDegree w p) : WithBot M)

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

Premises used: MvPolynomial.weightedTotalDegree, MvPolynomial.weightedTotalDegree', 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
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
b : σ →₀ ℕ
⊢ b ∈ p.support →
    LE.le.{u_2} (α := M) ((weight w : (a : σ →₀ ℕ) → M) b : M)
      (p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s : M)

Tactic:
Finset.le_sup

Premises used: 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
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
b : σ →₀ ℕ
⊢ b ∈ p.support →
    LE.le.{u_2} (α := M) ((weight w : (a : σ →₀ ℕ) → M) b : M)
      (p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s : M)

Tactic:
exact Finset.le_sup

Premises used: 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
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p ≤ (↑m : WithBot M)

Tactic:
have hm' : weightedTotalDegree' w p ≤ m := le_of_eq hm.symm
-- 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
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
hm' : weightedTotalDegree' w p ≤ (↑m : WithBot M)
a : (↑(p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) ≤ (↑m : WithBot M)
⊢ (↑(p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) ≤ weightedTotalDegree' w p

Tactic:
rw [← 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
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : (↑m : WithBot M) = weightedTotalDegree' w p
hm' : weightedTotalDegree' w p ≤ (↑m : WithBot M)
⊢ (↑(p.support.sup fun (s : σ →₀ ℕ) ↦ (weight w : (a : σ →₀ ℕ) → M) s) : WithBot M) ≤ (↑m : WithBot M)

Tactic:
simpa [weightedTotalDegree'] using hm'

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
⊢ weightedTotalDegree.{u_1, u_2, u_3} (R := R) w 0 = ⊥

Tactic:
simp only [weightedTotalDegree, support_zero, Finset.sup_empty]

Premises used: MvPolynomial.weightedTotalDegree, Finset.sup_empty, MvPolynomial.support_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
inst_2 : SemilatticeSup M
inst_3 : OrderBot M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (weight w : (a : σ →₀ ℕ) → M) d ≤ weightedTotalDegree w φ

Tactic:
le_sup hd

Premises used: MvPolynomial.weightedTotalDegree, 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
m : M
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} 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.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} 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.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} 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.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c a ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m

Tactic:
ha 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
m : M
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c a ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m

Tactic:
exact ha 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
m : M
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c b ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m

Tactic:
hb 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
m : M
a b : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
hb : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} b
c : σ →₀ ℕ
hc : coeff c a + coeff c b ≠ 0
h : coeff c b ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m

Tactic:
exact hb 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
m : M
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} 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.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
w : σ → M
m : M
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m

Tactic:
ha (right_ne_zero_of_mul hc)

Premises used: right_ne_zero_of_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
w : σ → M
m : M
r : R
a : MvPolynomial σ R
ha : Membership.mem (γ := Set (MvPolynomial σ R)) {x : MvPolynomial σ R | IsWeightedHomogeneous w x m} a
c : σ →₀ ℕ
hc : r • coeff c a ≠ 0
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m

Tactic:
exact ha (right_ne_zero_of_mul hc)

Premises used: right_ne_zero_of_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
w : σ → M
m : M
p : MvPolynomial σ R
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) p ↔
    IsWeightedHomogeneous w p m

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, 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
w : σ → M
m : M
h :
  ∀ (x : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) x ↔
      Membership.mem (γ := Submodule R (MvPolynomial σ R))
        (Finsupp.supported R R {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m}) x
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
    (Finsupp.supported R R {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m})

Tactic:
ext x
-- 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
x : MvPolynomial σ R
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) x ↔
    ∀ (x_1 : σ →₀ ℕ),
      Ne.{u_1 + 1} (α := R) ((x : (a : σ →₀ ℕ) → R) x_1 : R) (0 : R) →
        Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} x_1
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) x ↔
    ∀ x_1 ∈ (↑x.support : Set (σ →₀ ℕ)),
      Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} x_1

Tactic:
simp only [Finsupp.mem_support_iff, mem_coe]

Premises used: Finsupp.mem_support_iff, Finset.mem_coe
-- 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
x : MvPolynomial σ R
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) x ↔
    ∀ (x_1 : σ →₀ ℕ),
      Ne.{u_1 + 1} (α := R) ((x : (a : σ →₀ ℕ) → R) x_1 : R) (0 : R) →
        Membership.mem (γ := Set (σ →₀ ℕ)) {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → M) d = m} x_1

Tactic:
rfl
-- 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 n : M
rw :
  ∀ (m_1 : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) m_1 →
      ∀ (n_1 : MvPolynomial σ R),
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) n_1 →
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (m + n)) (m_1 * n_1)
⊢ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
      (weightedHomogeneousSubmodule R w n) ≤
    weightedHomogeneousSubmodule R w (m + n)

Tactic:
rw [Submodule.mul_le]

Premises used: Submodule.mul_le
-- 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 n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : coeff c (φ * ψ) ≠ 0
⊢ Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0

Tactic:
rw [coeff_mul] at hc

Premises used: MvPolynomial.coeff_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
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
obtain :
  ∀ (d e : σ →₀ ℕ) (hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c) (H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m + n
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m + n

Tactic:
obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc

Premises used: Finset.exists_ne_zero_of_sum_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
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
contrapose! : ∀ (H : ∀ (_ : coeff d φ ≠ 0), coeff e ψ = 0), coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
⊢ coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0

Tactic:
contrapose! 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
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : ∀ (_ : coeff d φ ≠ 0), coeff e ψ = 0
pos : ∀ (h : coeff d φ = 0), coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
neg : ∀ (h : ¬coeff d φ = 0), coeff (d, e).1 φ * coeff (d, e).2 ψ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0

Tactic:
by_cases h : coeff d φ = 0

Premises used: MvPolynomial.coeff
-- 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 n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : ∀ (_ : coeff d φ ≠ 0), coeff e ψ = 0
h : coeff d φ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0

Tactic:
simp_all only [Ne, not_false_iff, zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, Ne, MulZeroClass.mul_zero, 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
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : ∀ (_ : coeff d φ ≠ 0), coeff e ψ = 0
h : ¬coeff d φ = 0
⊢ coeff (d, e).1 φ * coeff (d, e).2 ψ = 0

Tactic:
simp_all only [Ne, not_false_iff, zero_mul, mul_zero]

Premises used: MulZeroClass.zero_mul, Ne, MulZeroClass.mul_zero, 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
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
⊢ coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0

Tactic:
have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
    contrapose! H
    by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_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
w : σ → M
m n : M
φ : MvPolynomial σ R
hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ
ψ : MvPolynomial σ R
hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ
c : σ →₀ ℕ
hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0
d e : σ →₀ ℕ
hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c
H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0
aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0
rw : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) = m + n
rw₁ : (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) = HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) n
rw₂ :
  (weight w : (a : σ →₀ ℕ) → M) ((d, e).1 + (d, e).2) =
    HAdd.hAdd (α := M) (β := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) e : M)
rw₃ rw₄ :
  HAdd.hAdd (α := M) (β := M) ((weight w : (a : σ →₀ ℕ) → M) (d, e).1 : M)
      ((weight w : (a : σ →₀ ℕ) → M) (d, e).2 : M) =
    HAdd.hAdd (α := M) (β := M) ((weight w : (a : σ →₀ ℕ) → M) d : M) ((weight w : (a : σ →₀ ℕ) → M) e : M)
⊢ (weight w : (a : σ →₀ ℕ) → M) c = m + n

Tactic:
rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]

Premises used: map_add, Finset.HasAntidiagonal.mem_antidiagonal, And.right, And.left, Iff.mp
-- 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 n : M
rw rw₁ rw₂ :
  ∀ (m_1 : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) m_1 →
      ∀ (n_1 : MvPolynomial σ R),
        Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) n_1 →
          Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w (m + n)) (m_1 * n_1)
rw₃ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : coeff c (φ * ψ) ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m + n
rw₄ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m + n
rw₅ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0) (d e : σ →₀ ℕ)
    (hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c) (H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0),
    (weight w : (a : σ →₀ ℕ) → M) c = m + n
rw₆ :
  ∀ (φ : MvPolynomial σ R)
    (hφ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m) φ)
    (ψ : MvPolynomial σ R)
    (hψ : Membership.mem (γ := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w n) ψ) ⦃c : σ →₀ ℕ⦄
    (hc : Ne.{u_1 + 1} (α := R) (∑ x ∈ @antidiagonal _ instAddMonoid _ c, coeff x.1 φ * coeff x.2 ψ) 0) (d e : σ →₀ ℕ)
    (hde : (d, e) ∈ @antidiagonal _ instAddMonoid _ c) (H : coeff (d, e).1 φ * coeff (d, e).2 ψ ≠ 0)
    (aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0), (weight w : (a : σ →₀ ℕ) → M) c = m + n
⊢ HMul.hMul (α := Submodule R (MvPolynomial σ R)) (weightedHomogeneousSubmodule R w m)
      (weightedHomogeneousSubmodule R w n) ≤
    weightedHomogeneousSubmodule R w (m + n)

Tactic:
classical
  rw [Submodule.mul_le]
  intro φ hφ ψ hψ c hc
  rw [coeff_mul] at hc
  obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
  have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
    contrapose! H
    by_cases h : coeff d φ = 0 <;>
      simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
  rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]

Premises used: map_add, Submodule.mul_le, MvPolynomial.coeff_mul