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

State before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Tactic:
obtain ⟨p, hp0, hpx⟩ := (mem_grade_iff' _ _ _).mp x.2
State after:
case intro.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x

State before:
case intro.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Tactic:
suffices ∃ (a : R), p.val = C a by
  obtain ⟨a, ha⟩ := this
  simp only [← hpx, ha, mk_C, AlgHom.commutes, Algebra.id.map_eq_id, RingHom.id_apply]
State after:
case intro.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ ∃ a, ↑p = C a

State before:
case intro.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ ∃ a, ↑p = C a
Tactic:
use constantCoeff p.val
State after:
case h
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ ↑p = C (constantCoeff ↑p)

State before:
case h
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
⊢ ↑p = C (constantCoeff ↑p)
Tactic:
ext exp
State after:
case h.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
⊢ coeff exp ↑p = coeff exp (C (constantCoeff ↑p))

State before:
case h.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
⊢ coeff exp ↑p = coeff exp (C (constantCoeff ↑p))
Tactic:
simp only [coeff_C]
State after:
case h.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
⊢ coeff exp ↑p = if 0 = exp then constantCoeff ↑p else 0

State before:
case h.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
⊢ coeff exp ↑p = if 0 = exp then constantCoeff ↑p else 0
Tactic:
split_ifs with hexp
State after:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : 0 = exp
⊢ coeff exp ↑p = constantCoeff ↑p

case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0

State before:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : 0 = exp
⊢ coeff exp ↑p = constantCoeff ↑p

case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Tactic:
. rw [← hexp, constantCoeff_eq]
State after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0

State before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Tactic:
. simp only [IsWeightedHomogeneous] at hp0
  by_contra h
  rw [eq_comm, ← Finsupp.support_eq_empty] at hexp
  obtain  ⟨nm, hnm⟩ := nonempty_of_ne_empty hexp
  specialize hp0 h
  simp only [weightedDegree, LinearMap.toAddMonoidHom_coe, Finsupp.total_apply, Finsupp.sum,
    sum_eq_zero_iff] at hp0
  specialize hp0 nm hnm
  simp only [smul_eq_mul, mul_eq_zero] at hp0
  cases' hp0 with hnm0 hnm0
  . simp only [Finsupp.mem_support_iff] at hnm
    exact hnm hnm0
  . apply lt_irrefl 0
    nth_rewrite 2 [← hnm0]
    apply MvPolynomial.mem_supported.mp p.prop
    simp only [mem_coe, mem_vars, Finsupp.mem_support_iff, ne_eq, mem_support_iff, exists_prop]
    simp only [Finsupp.mem_support_iff] at hnm
    exact ⟨exp, h, hnm⟩
State after:
no goals

State before:
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
this : ∃ a, ↑p = C a
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Tactic:
obtain ⟨a, ha⟩ := this
State after:
case intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
a : R
ha : ↑p = C a
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x

State before:
case intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
a : R
ha : ↑p = C a
⊢ (algebraMap R (DividedPowerAlgebra R M)) ((algebraMapInv R M) ↑x) = ↑x
Tactic:
simp only [← hpx, ha, mk_C, AlgHom.commutes, Algebra.id.map_eq_id, RingHom.id_apply]
State after:
no goals

State before:
case pos
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : 0 = exp
⊢ coeff exp ↑p = constantCoeff ↑p
Tactic:
rw [← hexp, constantCoeff_eq]
State after:
no goals

State before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : IsWeightedHomogeneous Prod.fst (↑p) 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Tactic:
simp only [IsWeightedHomogeneous] at hp0
State after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0

State before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
⊢ coeff exp ↑p = 0
Tactic:
by_contra h
State after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
h : ¬coeff exp ↑p = 0
⊢ False

State before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬0 = exp
h : ¬coeff exp ↑p = 0
⊢ False
Tactic:
rw [eq_comm, ← Finsupp.support_eq_empty] at hexp
State after:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
⊢ False

State before:
case neg
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
⊢ False
Tactic:
obtain  ⟨nm, hnm⟩ := nonempty_of_ne_empty hexp
State after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
⊢ False

State before:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hp0 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, coeff d ↑p ≠ 0 → (weightedDegree Prod.fst) d = 0
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
⊢ False
Tactic:
specialize hp0 h
State after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : (weightedDegree Prod.fst) exp = 0
⊢ False

State before:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : (weightedDegree Prod.fst) exp = 0
⊢ False
Tactic:
simp only [weightedDegree, LinearMap.toAddMonoidHom_coe, Finsupp.total_apply, Finsupp.sum,
  sum_eq_zero_iff] at hp0
State after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : ∀ x ∈ exp.support, exp x • x.1 = 0
⊢ False

State before:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : ∀ x ∈ exp.support, exp x • x.1 = 0
⊢ False
Tactic:
specialize hp0 nm hnm
State after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : exp nm • nm.1 = 0
⊢ False

State before:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : exp nm • nm.1 = 0
⊢ False
Tactic:
simp only [smul_eq_mul, mul_eq_zero] at hp0
State after:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : exp nm = 0 ∨ nm.1 = 0
⊢ False

State before:
case neg.intro
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hp0 : exp nm = 0 ∨ nm.1 = 0
⊢ False
Tactic:
cases' hp0 with hnm0 hnm0
State after:
case neg.intro.inl
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : exp nm = 0
⊢ False

case neg.intro.inr
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ False

State before:
case neg.intro.inl
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : exp nm = 0
⊢ False

case neg.intro.inr
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ False
Tactic:
. simp only [Finsupp.mem_support_iff] at hnm
  exact hnm hnm0
State after:
case neg.intro.inr
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ False

State before:
case neg.intro.inr
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ False
Tactic:
. apply lt_irrefl 0
  nth_rewrite 2 [← hnm0]
  apply MvPolynomial.mem_supported.mp p.prop
  simp only [mem_coe, mem_vars, Finsupp.mem_support_iff, ne_eq, mem_support_iff, exists_prop]
  simp only [Finsupp.mem_support_iff] at hnm
  exact ⟨exp, h, hnm⟩
State after:
no goals

State before:
case neg.intro.inl
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : exp nm = 0
⊢ False
Tactic:
simp only [Finsupp.mem_support_iff] at hnm
State after:
case neg.intro.inl
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm0 : exp nm = 0
hnm : exp nm ≠ 0
⊢ False

State before:
case neg.intro.inl
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm0 : exp nm = 0
hnm : exp nm ≠ 0
⊢ False
Tactic:
exact hnm hnm0
State after:
no goals

State before:
case neg.intro.inr
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ False
Tactic:
apply lt_irrefl 0
State after:
case neg.intro.inr
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ 0 < 0

State before:
case neg.intro.inr
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ 0 < 0
Tactic:
nth_rewrite 2 [← hnm0]
State after:
case neg.intro.inr
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ 0 < nm.1

State before:
case neg.intro.inr
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ 0 < nm.1
Tactic:
apply MvPolynomial.mem_supported.mp p.prop
State after:
case neg.intro.inr.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ nm ∈ ↑(↑p).vars

State before:
case neg.intro.inr.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ nm ∈ ↑(↑p).vars
Tactic:
simp only [mem_coe, mem_vars, Finsupp.mem_support_iff, ne_eq, mem_support_iff, exists_prop]
State after:
case neg.intro.inr.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ ∃ d, ¬coeff d ↑p = 0 ∧ ¬d nm = 0

State before:
case neg.intro.inr.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm : nm ∈ exp.support
hnm0 : nm.1 = 0
⊢ ∃ d, ¬coeff d ↑p = 0 ∧ ¬d nm = 0
Tactic:
simp only [Finsupp.mem_support_iff] at hnm
State after:
case neg.intro.inr.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm0 : nm.1 = 0
hnm : exp nm ≠ 0
⊢ ∃ d, ¬coeff d ↑p = 0 ∧ ¬d nm = 0

State before:
case neg.intro.inr.a
R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ↥(grade R M 0)
p : ↥(supported R {nm | 0 < nm.1})
hpx : mk ↑p = ↑x
exp : ℕ × M →₀ ℕ
hexp : ¬exp.support = ∅
h : ¬coeff exp ↑p = 0
nm : ℕ × M
hnm0 : nm.1 = 0
hnm : exp nm ≠ 0
⊢ ∃ d, ¬coeff d ↑p = 0 ∧ ¬d nm = 0
Tactic:
exact ⟨exp, h, hnm⟩
State after:
no goals