internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal
Proof 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⟩⟩
Proof 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
Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal
Proof 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']
Proof 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
Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal
Proof 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)
Proof state after:
no goals
Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal
Proof 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⟩⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal
Proof 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'
Proof 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
Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal
Proof 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']
Proof state after:
no goals
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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 ⊢
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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]
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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 _ _
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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]
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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]
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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 _ _ _
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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]
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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]
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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)))
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof state after:
no goals
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.augIdeal_eq_span
Proof 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)
Proof state after:
no goals