-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedDegree_eq_zero_iff [CanonicallyOrderedAdd M]
    (hw : NonTorsionWeight w) {m : σ →₀ ℕ} :
    weight w m = 0 ↔ ∀ x : σ, m x = 0

Proof state:
case h
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ x ∈ m.support → m x • w x = 0 ↔ m x = 0

Tactic:
rw [Finsupp.mem_support_iff]

Result:
case h
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ m x ≠ 0 → m x • w x = 0 ↔ m x = 0

Proof state:
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ (∀ x ∈ m.support, m x • w x = 0) ↔ ∀ (x : σ), m x = 0

Tactic:
apply forall_congr'

Result:
case h
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ ∀ (a : σ), a ∈ m.support → m a • w a = 0 ↔ m a = 0

Proof state:
case h
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ ∀ (a : σ), a ∈ m.support → m a • w a = 0 ↔ m a = 0

Tactic:
intro x

Result:
case h
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ x ∈ m.support → m x • w x = 0 ↔ m x = 0

Proof state:
case h.mp
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
hx : m x ≠ 0 → m x • w x = 0
⊢ m x = 0

Tactic:
by_contra hx'

Result:
case h.mp
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
hx : m x ≠ 0 → m x • w x = 0
hx' : ¬m x = 0
⊢ False

Proof state:
case h.mp
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ (m x ≠ 0 → m x • w x = 0) → m x = 0

Tactic:
intro hx

Result:
case h.mp
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
hx : m x ≠ 0 → m x • w x = 0
⊢ m x = 0

Proof state:
case h.mp
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
hx : m x ≠ 0 → m x • w x = 0
hx' : ¬m x = 0
⊢ False

Tactic:
exact absurd (hw _ _ (hx hx')) hx'

Result:
no goals

Proof state:
case h.mpr
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ m x = 0 → m x ≠ 0 → m x • w x = 0

Tactic:
intro hax _

Result:
case h.mpr
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
hax : m x = 0
a✝ : m x ≠ 0
⊢ m x • w x = 0

Proof state:
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ (weight w) m = 0 ↔ ∀ (x : σ), m x = 0

Tactic:
simp only [weight, Finsupp.linearCombination, LinearMap.toAddMonoidHom_coe, coe_lsum,
  LinearMap.coe_smulRight, LinearMap.id_coe, id_eq]

Result:
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ (m.sum fun i c => c • w i) = 0 ↔ ∀ (x : σ), m x = 0

Proof state:
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ (m.sum fun i c => c • w i) = 0 ↔ ∀ (x : σ), m x = 0

Tactic:
rw [Finsupp.sum, Finset.sum_eq_zero_iff]

Result:
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
⊢ (∀ x ∈ m.support, m x • w x = 0) ↔ ∀ (x : σ), m x = 0

Proof state:
case h
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ m x ≠ 0 → m x • w x = 0 ↔ m x = 0

Tactic:
constructor

Result:
case h.mp
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ (m x ≠ 0 → m x • w x = 0) → m x = 0

case h.mpr
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
⊢ m x = 0 → m x ≠ 0 → m x • w x = 0

Proof state:
case h.mpr
M : Type u_2
σ : Type u_3
inst✝¹ : OrderedAddCommMonoid M
w : σ → M
inst✝ : CanonicallyOrderedAdd M
hw : NonTorsionWeight w
m : σ →₀ ℕ
x : σ
hax : m x = 0
a✝ : m x ≠ 0
⊢ m x • w x = 0

Tactic:
simp only [hax, zero_smul]

Result:
no goals