Theorem: MvPolynomial.decompose'_aux (DividedPowers/ForMathlib/WeightedHomogeneous.lean)

State before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ (weightedHomogeneousComponent w i) φ = 0
Tactic:
apply weightedHomogeneousComponent_eq_zero'
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ∀ d ∈ φ.support, (weightedDegree w) d ≠ i

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ∀ d ∈ φ.support, (weightedDegree w) d ≠ i
Tactic:
simp only [Finset.mem_image, mem_support_iff, ne_eq, exists_prop, not_exists, not_and] at hi
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
⊢ ∀ d ∈ φ.support, (weightedDegree w) d ≠ i

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
⊢ ∀ d ∈ φ.support, (weightedDegree w) d ≠ i
Tactic:
intro m hm
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : m ∈ φ.support
⊢ (weightedDegree w) m ≠ i

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : m ∈ φ.support
⊢ (weightedDegree w) m ≠ i
Tactic:
apply hi m
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : m ∈ φ.support
⊢ ¬coeff m φ = 0

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : m ∈ φ.support
⊢ ¬coeff m φ = 0
Tactic:
rw [mem_support_iff] at hm
State after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : coeff m φ ≠ 0
⊢ ¬coeff m φ = 0

State before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : coeff m φ ≠ 0
⊢ ¬coeff m φ = 0
Tactic:
exact hm
State after:
no goals