Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : mk f ∈ augIdeal R M
⊢ coeff 0 f = 0
Tactic:
simp only [augIdeal, AlgHom.toRingHom_eq_coe, RingHom.mem_ker, RingHom.coe_coe] at hf0
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ coeff 0 f = 0

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ coeff 0 f = 0
Tactic:
rw [← hf0, algebraMapInv_eq R M, eq_comm]
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) f = coeff 0 f

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) f = coeff 0 f
Tactic:
conv_lhs => rw [f.as_sum]
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) (∑ v ∈ f.support, (monomial v) (coeff v f)) = coeff 0 f

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) (∑ v ∈ f.support, (monomial v) (coeff v f)) = coeff 0 f
Tactic:
rw [map_sum, Finset.sum_eq_single 0]
State after:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial 0) (coeff 0 f)) = coeff 0 f

case h₀
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ ∀ b ∈ f.support, b ≠ 0 → (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial b) (coeff b f)) = 0

case h₁
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ 0 ∉ f.support → (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial 0) (coeff 0 f)) = 0

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial 0) (coeff 0 f)) = coeff 0 f

case h₀
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ ∀ b ∈ f.support, b ≠ 0 → (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial b) (coeff b f)) = 0

case h₁
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ 0 ∉ f.support → (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial 0) (coeff 0 f)) = 0
Tactic:
. simp only [monomial_zero', aeval_C, Algebra.id.map_eq_id, RingHom.id_apply]
State after:
case h₀
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ ∀ b ∈ f.support, b ≠ 0 → (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial b) (coeff b f)) = 0

case h₁
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ 0 ∉ f.support → (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial 0) (coeff 0 f)) = 0

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial 0) (coeff 0 f)) = coeff 0 f
Tactic:
simp only [monomial_zero', aeval_C, Algebra.id.map_eq_id, RingHom.id_apply]
State after:
no goals

State before:
case h₀
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ ∀ b ∈ f.support, b ≠ 0 → (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial b) (coeff b f)) = 0
Tactic:
intro b hb hb0
State after:
case h₀
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial b) (coeff b f)) = 0

State before:
case h₀
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial b) (coeff b f)) = 0
Tactic:
rw [aeval_monomial, Algebra.id.map_eq_id, RingHom.id_apply]
State after:
case h₀
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
⊢ (coeff b f * b.prod fun i k => (if 0 < i.1 then 0 else 1) ^ k) = 0

State before:
case h₀
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
⊢ (coeff b f * b.prod fun i k => (if 0 < i.1 then 0 else 1) ^ k) = 0
Tactic:
convert mul_zero (coeff b f)
State after:
case h.e'_2.h.e'_6
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
⊢ (b.prod fun i k => (if 0 < i.1 then 0 else 1) ^ k) = 0

State before:
case h.e'_2.h.e'_6
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
⊢ (b.prod fun i k => (if 0 < i.1 then 0 else 1) ^ k) = 0
Tactic:
obtain ⟨i, hi⟩ := Finsupp.support_nonempty_iff.mpr hb0
State after:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ (b.prod fun i k => (if 0 < i.1 then 0 else 1) ^ k) = 0

State before:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ (b.prod fun i k => (if 0 < i.1 then 0 else 1) ^ k) = 0
Tactic:
rw [Finsupp.prod]
State after:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ ∏ a ∈ b.support, (if 0 < a.1 then 0 else 1) ^ b a = 0

State before:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ ∏ a ∈ b.support, (if 0 < a.1 then 0 else 1) ^ b a = 0
Tactic:
apply Finset.prod_eq_zero hi
State after:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ (if 0 < i.1 then 0 else 1) ^ b i = 0

State before:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ (if 0 < i.1 then 0 else 1) ^ b i = 0
Tactic:
have hi' : 0 < i.fst := by
  apply mem_supported.mp hf
  rw [Finset.mem_coe, mem_vars]
  exact ⟨b, ⟨hb, hi⟩⟩
State after:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
hi' : 0 < i.1
⊢ (if 0 < i.1 then 0 else 1) ^ b i = 0

State before:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
hi' : 0 < i.1
⊢ (if 0 < i.1 then 0 else 1) ^ b i = 0
Tactic:
rw [if_pos hi']
State after:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
hi' : 0 < i.1
⊢ 0 ^ b i = 0

State before:
case h.e'_2.h.e'_6.intro
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
hi' : 0 < i.1
⊢ 0 ^ b i = 0
Tactic:
exact zero_pow (Finsupp.mem_support_iff.mp hi)
State after:
no goals

State before:
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ 0 < i.1
Tactic:
apply mem_supported.mp hf
State after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ i ∈ ↑f.vars

State before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ i ∈ ↑f.vars
Tactic:
rw [Finset.mem_coe, mem_vars]
State after:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ ∃ d ∈ f.support, i ∈ d.support

State before:
case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
b : ℕ × M →₀ ℕ
hb : b ∈ f.support
hb0 : b ≠ 0
i : ℕ × M
hi : i ∈ b.support
⊢ ∃ d ∈ f.support, i ∈ d.support
Tactic:
exact ⟨b, ⟨hb, hi⟩⟩
State after:
no goals

State before:
case h₁
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
⊢ 0 ∉ f.support → (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial 0) (coeff 0 f)) = 0
Tactic:
intro hf'
State after:
case h₁
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
hf' : 0 ∉ f.support
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial 0) (coeff 0 f)) = 0

State before:
case h₁
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
f : MvPolynomial (ℕ × M) R
hf : f ∈ supported R {nm | 0 < nm.1}
hf0 : (algebraMapInv R M) (mk f) = 0
hf' : 0 ∉ f.support
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) ((monomial 0) (coeff 0 f)) = 0
Tactic:
rw [monomial_zero', aeval_C, Algebra.id.map_eq_id, RingHom.id_apply, ←
  not_mem_support_iff.mp hf']
State after:
no goals