internlm/Lean-Github huggingface dataset:
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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
Proof state after:
no goals
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.algebraMap_right_inv_of_degree_zero
Proof 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⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mem_augIdeal_iff
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 : DividedPowerAlgebra R M
⊢ f ∈ augIdeal R M ↔ (algebraMapInv R M) f = 0
Tactic:
rw [augIdeal, RingHom.mem_ker]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_mem_augIdeal_iff
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
inst✝ : Nontrivial R
n : ℕ
m : M
⊢ dp R n m ∈ augIdeal R M ↔ 0 < n
Tactic:
rw [mem_augIdeal_iff, dp, algebraMapInv_eq, aeval_X]
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
inst✝ : Nontrivial R
n : ℕ
m : M
⊢ (if 0 < (n, m).1 then 0 else 1) = 0 ↔ 0 < n
Theorem: DividedPowerAlgebra.dp_mem_augIdeal_iff
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
inst✝ : Nontrivial R
n : ℕ
m : M
⊢ (if 0 < (n, m).1 then 0 else 1) = 0 ↔ 0 < n
Tactic:
simp only [ite_eq_left_iff, not_not, one_ne_zero, imp_false]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_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
n : ℕ
hn : 0 < n
m : M
⊢ dp R n m ∈ augIdeal R M
Tactic:
rw [mem_augIdeal_iff, dp, algebraMapInv_eq, aeval_X, if_pos hn]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.ι_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
m : M
⊢ (ι R M) m ∈ augIdeal R M
Tactic:
simp only [mem_augIdeal_iff, ι_def, dp, algebraMapInv_eq, aeval_X, zero_lt_one, ite_true]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.augIdeal_isAugmentationIdeal'
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
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (Ideal.Quotient.mk (augIdeal R M)) ((algebraMap_comp_kerLiftAlg R M) r) = r
Tactic:
dsimp only [algebraMap_comp_kerLiftAlg]
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
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (Ideal.Quotient.mk (augIdeal R M))
      (((algebraMap R (DividedPowerAlgebra R M)).comp (kerLiftAlg_algebraMapInv R M).toRingHom) r) =
    r
Theorem: DividedPowerAlgebra.augIdeal_isAugmentationIdeal'
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
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (Ideal.Quotient.mk (augIdeal R M))
      (((algebraMap R (DividedPowerAlgebra R M)).comp (kerLiftAlg_algebraMapInv R M).toRingHom) r) =
    r
Tactic:
rw [RingHom.coe_comp, Function.comp_apply, Ideal.Quotient.mk_algebraMap]
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
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (algebraMap R (DividedPowerAlgebra R M ⧸ augIdeal R M)) ((kerLiftAlg_algebraMapInv R M).toRingHom r) = r
Theorem: DividedPowerAlgebra.augIdeal_isAugmentationIdeal'
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
r : DividedPowerAlgebra R M ⧸ augIdeal R M
⊢ (algebraMap R (DividedPowerAlgebra R M ⧸ augIdeal R M)) ((kerLiftAlg_algebraMapInv R M).toRingHom r) = r
Tactic:
apply kerLiftAlg_rightInverse
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 : 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
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 : (algebraMapInv R M) (mk f) = 0
⊢ coeff 0 f = 0
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
⊢ coeff 0 f = 0
Tactic:
rw [← hf0, algebraMapInv_eq R M, eq_comm]
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 : (algebraMapInv R M) (mk f) = 0
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) f = coeff 0 f
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
⊢ (aeval fun nm => if 0 < nm.1 then 0 else 1) f = coeff 0 f
Tactic:
conv_lhs => rw [f.as_sum]
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 : (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
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
⊢ (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]
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 : (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
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
⊢ (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]
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
⊢ ∀ 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
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
⊢ (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]
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
⊢ ∀ 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
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
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
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
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]
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
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
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
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)
Proof 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
Theorem: DividedPowerAlgebra.coeff_zero_of_mem_augIdeal
Proof 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
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
⊢ (b.prod fun i k => (if 0 < i.1 then 0 else 1) ^ k) = 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
⊢ (b.prod fun i k => (if 0 < i.1 then 0 else 1) ^ k) = 0
Tactic:
rw [Finsupp.prod]
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
⊢ ∏ a ∈ b.support, (if 0 < a.1 then 0 else 1) ^ b a = 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
⊢ ∏ a ∈ b.support, (if 0 < a.1 then 0 else 1) ^ b a = 0
Tactic:
apply Finset.prod_eq_zero 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
⊢ (if 0 < i.1 then 0 else 1) ^ b i = 0