Theorem: DividedPowerAlgebra.augIdeal_eq_span (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
⊢ augIdeal R M = span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
apply le_antisymm
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
⊢ augIdeal R M ≤ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

case a
R : Type u
M : Type v
inst✝⁴ : CommRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ span (Set.image2 (dp R) {n | 0 < n} Set.univ) ≤ augIdeal R M

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
⊢ augIdeal R M ≤ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
intro f0 hf0
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
f0 : DividedPowerAlgebra R M
hf0 : f0 ∈ augIdeal R M
⊢ f0 ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

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
f0 : DividedPowerAlgebra R M
hf0 : f0 ∈ augIdeal R M
⊢ f0 ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
obtain ⟨⟨f, hf⟩, rfl⟩ := surjective_of_supported R M f0
State after:
case a.intro.mk
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.comp (supported R {nm | 0 < nm.1}).val) ⟨f, hf⟩ ∈ augIdeal R M
⊢ (mk.comp (supported R {nm | 0 < nm.1}).val) ⟨f, hf⟩ ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case a.intro.mk
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.comp (supported R {nm | 0 < nm.1}).val) ⟨f, hf⟩ ∈ augIdeal R M
⊢ (mk.comp (supported R {nm | 0 < nm.1}).val) ⟨f, hf⟩ ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
have hf0' : coeff 0 f = 0 := coeff_zero_of_mem_augIdeal R M hf hf0
State after:
case a.intro.mk
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.comp (supported R {nm | 0 < nm.1}).val) ⟨f, hf⟩ ∈ augIdeal R M
hf0' : coeff 0 f = 0
⊢ (mk.comp (supported R {nm | 0 < nm.1}).val) ⟨f, hf⟩ ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case a.intro.mk
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.comp (supported R {nm | 0 < nm.1}).val) ⟨f, hf⟩ ∈ augIdeal R M
hf0' : coeff 0 f = 0
⊢ (mk.comp (supported R {nm | 0 < nm.1}).val) ⟨f, hf⟩ ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
simp only [AlgHom.coe_comp, mkₐ_eq_mk, Subalgebra.coe_val, Function.comp_apply] at hf0 ⊢
State after:
case a.intro.mk
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
hf0' : coeff 0 f = 0
⊢ mk f ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case a.intro.mk
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
hf0' : coeff 0 f = 0
⊢ mk f ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
rw [f.as_sum, map_sum]
State after:
case a.intro.mk
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
hf0' : coeff 0 f = 0
⊢ ∑ x ∈ f.support, mk ((monomial x) (coeff x f)) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case a.intro.mk
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
hf0' : coeff 0 f = 0
⊢ ∑ x ∈ f.support, mk ((monomial x) (coeff x f)) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
refine' Ideal.sum_mem _ _
State after:
case a.intro.mk
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
hf0' : coeff 0 f = 0
⊢ ∀ c ∈ f.support, mk ((monomial c) (coeff c f)) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case a.intro.mk
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
hf0' : coeff 0 f = 0
⊢ ∀ c ∈ f.support, mk ((monomial c) (coeff c f)) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
intro c hc
State after:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
⊢ mk ((monomial c) (coeff c f)) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
⊢ mk ((monomial c) (coeff c f)) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
rw [monomial_eq, Finsupp.prod]
State after:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
⊢ mk (C (coeff c f) * ∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
⊢ mk (C (coeff c f) * ∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
simp only [_root_.map_mul]
State after:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
⊢ mk (C (coeff c f)) * mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
⊢ mk (C (coeff c f)) * mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
refine' mul_mem_left _ _ _
State after:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
by_cases hc0 : c.support.Nonempty
State after:
case pos
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
hc0 : c.support.Nonempty
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

case neg
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
hc0 : ¬c.support.Nonempty
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case pos
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
hc0 : c.support.Nonempty
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
obtain ⟨⟨n, m⟩, hnm⟩ := hc0
State after:
case pos.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
n : ℕ
m : M
hnm : (n, m) ∈ c.support
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case pos.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
n : ℕ
m : M
hnm : (n, m) ∈ c.support
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
rw [Finset.prod_eq_mul_prod_diff_singleton hnm]
State after:
case pos.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
n : ℕ
m : M
hnm : (n, m) ∈ c.support
⊢ mk (X (n, m) ^ c (n, m) * ∏ x ∈ c.support \ {(n, m)}, X x ^ c x) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case pos.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
n : ℕ
m : M
hnm : (n, m) ∈ c.support
⊢ mk (X (n, m) ^ c (n, m) * ∏ x ∈ c.support \ {(n, m)}, X x ^ c x) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
simp only [_root_.map_mul, map_pow]
State after:
case pos.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
n : ℕ
m : M
hnm : (n, m) ∈ c.support
⊢ mk (X (n, m)) ^ c (n, m) * mk (∏ x ∈ c.support \ {(n, m)}, X x ^ c x) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case pos.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
n : ℕ
m : M
hnm : (n, m) ∈ c.support
⊢ mk (X (n, m)) ^ c (n, m) * mk (∏ x ∈ c.support \ {(n, m)}, X x ^ c x) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
apply
  mul_mem_right _ _
    (pow_mem_of_mem _ _ _ (Nat.pos_of_ne_zero (Finsupp.mem_support_iff.mp hnm)))
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 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
n : ℕ
m : M
hnm : (n, m) ∈ c.support
⊢ mk (X (n, m)) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
n : ℕ
m : M
hnm : (n, m) ∈ c.support
⊢ mk (X (n, m)) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
refine subset_span ⟨n,
  by simpa only [Set.mem_setOf_eq] using supp_ss hnm,
  m, trivial , rfl⟩
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 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
n : ℕ
m : M
hnm : (n, m) ∈ c.support
⊢ n ∈ {n | 0 < n}
Tactic:
simpa only [Set.mem_setOf_eq] using supp_ss hnm
State after:
no goals

State before:
case neg
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
hc0 : ¬c.support.Nonempty
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
rw [not_nonempty_iff_eq_empty, Finsupp.support_eq_empty] at hc0
State after:
case neg
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
hc0 : c = 0
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case neg
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
hc0 : c = 0
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
rw [hc0] at hc
State after:
case neg
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : 0 ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
hc0 : c = 0
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)

State before:
case neg
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : 0 ∈ f.support
supp_ss : ↑c.support ⊆ {nm | 0 < nm.1}
hc0 : c = 0
⊢ mk (∏ a ∈ c.support, X a ^ c a) ∈ span (Set.image2 (dp R) {n | 0 < n} Set.univ)
Tactic:
exact absurd hf0' (mem_support_iff.mp hc)
State after:
no goals

State before:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
⊢ ↑c.support ⊆ {nm | 0 < nm.1}
Tactic:
intro nm hnm
State after:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ nm ∈ {nm | 0 < nm.1}

State before:
case a.intro.mk
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
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ nm ∈ {nm | 0 < nm.1}
Tactic:
apply mem_supported.mp hf
State after:
case a.intro.mk.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 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ nm ∈ ↑f.vars

State before:
case a.intro.mk.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 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ nm ∈ ↑f.vars
Tactic:
simp only [mem_vars, mem_coe, mem_support_iff, ne_eq, Finsupp.mem_support_iff, exists_prop]
State after:
case a.intro.mk.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 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ ∃ d, ¬coeff d f = 0 ∧ ¬d nm = 0

State before:
case a.intro.mk.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 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : nm ∈ ↑c.support
⊢ ∃ d, ¬coeff d f = 0 ∧ ¬d nm = 0
Tactic:
rw [mem_coe, Finsupp.mem_support_iff] at hnm
State after:
case a.intro.mk.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 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : c nm ≠ 0
⊢ ∃ d, ¬coeff d f = 0 ∧ ¬d nm = 0

State before:
case a.intro.mk.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 : mk f ∈ augIdeal R M
hf0' : coeff 0 f = 0
c : ℕ × M →₀ ℕ
hc : c ∈ f.support
nm : ℕ × M
hnm : c nm ≠ 0
⊢ ∃ d, ¬coeff d f = 0 ∧ ¬d nm = 0
Tactic:
exact ⟨c, ⟨mem_support_iff.mp hc, hnm⟩⟩
State after:
no goals

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
⊢ span (Set.image2 (dp R) {n | 0 < n} Set.univ) ≤ augIdeal R M
Tactic:
rw [span_le]
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
⊢ Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑(augIdeal R M)

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
⊢ Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑(augIdeal R M)
Tactic:
intro f
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 : DividedPowerAlgebra R M
⊢ f ∈ Set.image2 (dp R) {n | 0 < n} Set.univ → f ∈ ↑(augIdeal R M)

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 : DividedPowerAlgebra R M
⊢ f ∈ Set.image2 (dp R) {n | 0 < n} Set.univ → f ∈ ↑(augIdeal R M)
Tactic:
simp only [Set.mem_image2, Set.mem_setOf_eq, Set.mem_univ, true_and_iff, exists_and_left,
  SetLike.mem_coe, forall_exists_index, and_imp]
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 : DividedPowerAlgebra R M
⊢ ∀ (x : ℕ), 0 < x → ∀ (x_1 : M), dp R x x_1 = f → f ∈ augIdeal R M

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 : DividedPowerAlgebra R M
⊢ ∀ (x : ℕ), 0 < x → ∀ (x_1 : M), dp R x x_1 = f → f ∈ augIdeal R M
Tactic:
intro n hn m 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 : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ f ∈ augIdeal R M

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 : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ f ∈ augIdeal R M
Tactic:
rw [← hf, mem_augIdeal_iff, algebraMapInv, liftAlgHom_apply_dp]
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 : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ (dividedPowersBot R).dpow n (0 m) = 0

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 : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ (dividedPowersBot R).dpow n (0 m) = 0
Tactic:
simp_rw [LinearMap.zero_apply]
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 : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ (dividedPowersBot R).dpow n 0 = 0

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 : DividedPowerAlgebra R M
n : ℕ
hn : 0 < n
m : M
hf : dp R n m = f
⊢ (dividedPowersBot R).dpow n 0 = 0
Tactic:
rw [DividedPowers.dpow_eval_zero _ (ne_of_gt hn)]
State after:
no goals