-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedTotalDegree_eq_zero_iff (hw : NonTorsionWeight w) (p : MvPolynomial σ R) :
    p.weightedTotalDegree w = 0 ↔ ∀ (m : σ →₀ ℕ) (_ : m ∈ p.support) (x : σ), m x = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weight w) d = 0) ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

Tactic:
apply forall_congr'

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ ∀ (a : σ →₀ ℕ), coeff a p ≠ 0 → (weight w) a = 0 ↔ a ∈ p.support → ∀ (x : σ), a x = 0

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff m p ≠ 0 → ((weight w) m = 0 ↔ ∀ (x : σ), m x = 0)

Tactic:
intro _

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
a✝ : coeff m p ≠ 0
⊢ (weight w) m = 0 ↔ ∀ (x : σ), m x = 0

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ ∀ (a : σ →₀ ℕ), coeff a p ≠ 0 → (weight w) a = 0 ↔ a ∈ p.support → ∀ (x : σ), a x = 0

Tactic:
intro m

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff m p ≠ 0 → (weight w) m = 0 ↔ m ∈ p.support → ∀ (x : σ), m x = 0

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff m p ≠ 0 → (weight w) m = 0 ↔ m ∈ p.support → ∀ (x : σ), m x = 0

Tactic:
rw [mem_support_iff]

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff m p ≠ 0 → (weight w) m = 0 ↔ coeff m p ≠ 0 → ∀ (x : σ), m x = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ weightedTotalDegree w p = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

Tactic:
rw [← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsWeightedHomogeneous]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
⊢ (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weight w) d = 0) ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
a✝ : coeff m p ≠ 0
⊢ (weight w) m = 0 ↔ ∀ (x : σ), m x = 0

Tactic:
exact weightedDegree_eq_zero_iff hw

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff m p ≠ 0 → (weight w) m = 0 ↔ coeff m p ≠ 0 → ∀ (x : σ), m x = 0

Tactic:
apply forall_congr'

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
hw : NonTorsionWeight w
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff m p ≠ 0 → ((weight w) m = 0 ↔ ∀ (x : σ), m x = 0)