internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case convert_2.hp
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ IsWeightedHomogeneous w (↑(x n)) n

case convert_2.a
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ m ≠ n
Tactic:
rw [← mem_weightedHomogeneousSubmodule]
Proof state after:
case convert_2.hp
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ ↑(x n) ∈ weightedHomogeneousSubmodule R w n

case convert_2.a
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ m ≠ n
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case convert_2.hp
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ ↑(x n) ∈ weightedHomogeneousSubmodule R w n

case convert_2.a
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ m ≠ n
Tactic:
exact (x n).prop
Proof state after:
case convert_2.a
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ m ≠ n
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case convert_2.a
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m n : M
a✝ : n ∈ DFinsupp.support x
hmn : n ≠ m
⊢ m ≠ n
Tactic:
exact Ne.symm hmn
Proof state after:
no goals
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case convert_3
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ m ∉ DFinsupp.support x → (weightedHomogeneousComponent w m) ↑(x m) = 0
Tactic:
rw [DFinsupp.not_mem_support_iff]
Proof state after:
case convert_3
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ x m = 0 → (weightedHomogeneousComponent w m) ↑(x m) = 0
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case convert_3
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m : M
⊢ x m = 0 → (weightedHomogeneousComponent w m) ↑(x m) = 0
Tactic:
intro hm
Proof state after:
case convert_3
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m : M
hm : x m = 0
⊢ (weightedHomogeneousComponent w m) ↑(x m) = 0
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case convert_3
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
σ : Type u_1
inst✝³ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : DirectSum M fun i => ↥(weightedHomogeneousSubmodule R w i)
m : M
hm : x m = 0
⊢ (weightedHomogeneousComponent w m) ↑(x m) = 0
Tactic:
rw [hm, Submodule.coe_zero, map_zero]
Proof state after:
no goals
Theorem: MvPolynomial.nonTorsionWeight_of_nonZero
Proof state before:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
⊢ NonTorsionWeight w
Tactic:
intro n x
Proof state after:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
⊢ n • w x = 0 → n = 0
Theorem: MvPolynomial.nonTorsionWeight_of_nonZero
Proof state before:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
⊢ n • w x = 0 → n = 0
Tactic:
rw [smul_eq_zero]
Proof state after:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
⊢ n = 0 ∨ w x = 0 → n = 0
Theorem: MvPolynomial.nonTorsionWeight_of_nonZero
Proof state before:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
⊢ n = 0 ∨ w x = 0 → n = 0
Tactic:
intro hnx
Proof state after:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hnx : n = 0 ∨ w x = 0
⊢ n = 0
Theorem: MvPolynomial.nonTorsionWeight_of_nonZero
Proof state before:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hnx : n = 0 ∨ w x = 0
⊢ n = 0
Tactic:
cases' hnx with hn hx
Proof state after:
case inl
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hn : n = 0
⊢ n = 0

case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ n = 0
Theorem: MvPolynomial.nonTorsionWeight_of_nonZero
Proof state before:
case inl
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hn : n = 0
⊢ n = 0

case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ n = 0
Tactic:
exact hn
Proof state after:
case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ n = 0
Theorem: MvPolynomial.nonTorsionWeight_of_nonZero
Proof state before:
case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ n = 0
Tactic:
exfalso
Proof state after:
case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ False
Theorem: MvPolynomial.nonTorsionWeight_of_nonZero
Proof state before:
case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ False
Tactic:
exact hw x hx
Proof state after:
no goals
Theorem: MvPolynomial.decompose'_aux
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ (weightedHomogeneousComponent w i) φ = 0
Tactic:
apply weightedHomogeneousComponent_eq_zero'
Proof state after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ∀ d ∈ φ.support, (weightedDegree w) d ≠ i
Theorem: MvPolynomial.decompose'_aux
Proof state before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ∀ d ∈ φ.support, (weightedDegree w) d ≠ i
Tactic:
simp only [Finset.mem_image, mem_support_iff, ne_eq, exists_prop, not_exists, not_and] at hi
Proof state after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
⊢ ∀ d ∈ φ.support, (weightedDegree w) d ≠ i
Theorem: MvPolynomial.decompose'_aux
Proof state before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
⊢ ∀ d ∈ φ.support, (weightedDegree w) d ≠ i
Tactic:
intro m hm
Proof state after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : m ∈ φ.support
⊢ (weightedDegree w) m ≠ i
Theorem: MvPolynomial.decompose'_aux
Proof state before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : m ∈ φ.support
⊢ (weightedDegree w) m ≠ i
Tactic:
apply hi m
Proof state after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : m ∈ φ.support
⊢ ¬coeff m φ = 0
Theorem: MvPolynomial.decompose'_aux
Proof state before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : m ∈ φ.support
⊢ ¬coeff m φ = 0
Tactic:
rw [mem_support_iff] at hm
Proof state after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : coeff m φ ≠ 0
⊢ ¬coeff m φ = 0
Theorem: MvPolynomial.decompose'_aux
Proof state before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weightedDegree w) x = i
m : σ →₀ ℕ
hm : coeff m φ ≠ 0
⊢ ¬coeff m φ = 0
Tactic:
exact hm
Proof state after:
no goals
Theorem: MvPolynomial.decompose'_toFun_apply
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ ↑((MvPolynomial.decompose'_toFun R w φ) m) = (weightedHomogeneousComponent w m) φ
Tactic:
rw [decompose'_toFun]
Proof state after:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Theorem: MvPolynomial.decompose'_toFun_apply
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Tactic:
by_cases hm : m ∈ Finset.image (weightedDegree w) φ.support
Proof state after:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∈ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Theorem: MvPolynomial.decompose'_toFun_apply
Proof state before:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∈ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Tactic:
simp only [DirectSum.mk_apply_of_mem hm, Subtype.coe_mk]
Proof state after:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Theorem: MvPolynomial.decompose'_toFun_apply
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
hm : m ∉ Finset.image (⇑(weightedDegree w)) φ.support
⊢ ↑(((DirectSum.mk (fun i => ↥(weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(weightedDegree w)) φ.support))
          fun m => ⟨(weightedHomogeneousComponent w ↑m) φ, ⋯⟩)
        m) =
    (weightedHomogeneousComponent w m) φ
Tactic:
rw [DirectSum.mk_apply_of_not_mem hm, Submodule.coe_zero, decompose'_aux w φ m hm]
Proof state after:
no goals
Theorem: Submodule.iSup_eq_span'
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_3
p : ι → Submodule R M
h : ι → Prop
⊢ ⨆ i, ⨆ (_ : h i), p i = span R (⋃ i, ⋃ (_ : h i), ↑(p i))
Tactic:
simp_rw [← Submodule.iSup_span, Submodule.span_eq]
Proof state after:
no goals
Theorem: Subideal.bot_def
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
⊢ ⟨⊥, ⋯⟩ = ⊥
Tactic:
rw [mk_bot]
Proof state after:
no goals
Theorem: Subideal.inf_def
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
⊢ J ⊓ J' = ⟨↑J ⊓ ↑J', ⋯⟩
Tactic:
ext x
Proof state after:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
⊢ x ∈ ↑(J ⊓ J') ↔ x ∈ ↑⟨↑J ⊓ ↑J', ⋯⟩
Theorem: Subideal.inf_def
Proof state before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
⊢ x ∈ ↑(J ⊓ J') ↔ x ∈ ↑⟨↑J ⊓ ↑J', ⋯⟩
Tactic:
exact ⟨fun ⟨h, _⟩ => h, fun h => ⟨h, J.property h.left⟩⟩
Proof state after:
no goals
Theorem: Subideal.sInf_def
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
⊢ sInf S = ⟨sInf (val '' S) ⊓ I, ⋯⟩
Tactic:
ext x
Proof state after:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
x : A
⊢ x ∈ ↑(sInf S) ↔ x ∈ ↑⟨sInf (val '' S) ⊓ I, ⋯⟩
Theorem: Subideal.sInf_def
Proof state before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
x : A
⊢ x ∈ ↑(sInf S) ↔ x ∈ ↑⟨sInf (val '' S) ⊓ I, ⋯⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Subideal.sup_def
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
⊢ J ⊔ J' = ⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩
Tactic:
ext x
Proof state after:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
⊢ x ∈ ↑(J ⊔ J') ↔ x ∈ ↑⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩
Theorem: Subideal.sup_def
Proof state before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
⊢ x ∈ ↑(J ⊔ J') ↔ x ∈ ↑⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩
Tactic:
refine' ⟨fun ⟨h, _⟩ => h, fun h => ⟨h, _⟩⟩
Proof state after:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
h : x ∈ ↑⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩
⊢ x ∈ ↑I
Theorem: Subideal.sup_def
Proof state before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
h : x ∈ ↑⟨sInf {B | ↑J ≤ B ∧ ↑J' ≤ B}, ⋯⟩
⊢ x ∈ ↑I
Tactic:
rw [coe_mk, Submodule.mem_sInf] at h
Proof state after:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
h : ∀ p ∈ {B | ↑J ≤ B ∧ ↑J' ≤ B}, x ∈ p
⊢ x ∈ ↑I
Theorem: Subideal.sup_def
Proof state before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
J J' : { J // J ≤ I }
x : A
h : ∀ p ∈ {B | ↑J ≤ B ∧ ↑J' ≤ B}, x ∈ p
⊢ x ∈ ↑I
Tactic:
exact h I ⟨J.2, J'.2⟩
Proof state after:
no goals
Theorem: Subideal.sSup_def
Proof state before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
⊢ sSup S = ⟨sSup (val '' S) ⊓ I, ⋯⟩
Tactic:
ext x
Proof state after:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
x : A
⊢ x ∈ ↑(sSup S) ↔ x ∈ ↑⟨sSup (val '' S) ⊓ I, ⋯⟩
Theorem: Subideal.sSup_def
Proof state before:
case a.h
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
S : Set { J // J ≤ I }
x : A
⊢ x ∈ ↑(sSup S) ↔ x ∈ ↑⟨sSup (val '' S) ⊓ I, ⋯⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
⊢ hI.isSubDPIdeal (J ⊓ I) ↔ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
Tactic:
refine' ⟨fun hIJ n a b ha hb hab => _, fun hIJ => _⟩
Proof state after:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
⊢ hI.dpow n a - hI.dpow n b ∈ J

case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
⊢ hI.isSubDPIdeal (J ⊓ I)
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
⊢ hI.dpow n a - hI.dpow n b ∈ J
Tactic:
have hab' : a - b ∈ I := I.sub_mem ha hb
Proof state after:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ hI.dpow n a - hI.dpow n b ∈ J
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ hI.dpow n a - hI.dpow n b ∈ J
Tactic:
rw [← add_sub_cancel b a, hI.dpow_add' n hb hab', Finset.range_succ,
  Finset.sum_insert Finset.not_mem_range_self, tsub_self, hI.dpow_zero hab', mul_one,
  add_sub_cancel_left]
Proof state after:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∑ x ∈ Finset.range n, hI.dpow x b * hI.dpow (n - x) (a - b) ∈ J
Theorem: DividedPowers.isSubDPIdeal_inf_iff
Proof state before:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∑ x ∈ Finset.range n, hI.dpow x b * hI.dpow (n - x) (a - b) ∈ J
Tactic:
apply Ideal.sum_mem
Proof state after:
case refine'_1.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∀ c ∈ Finset.range n, hI.dpow c b * hI.dpow (n - c) (a - b) ∈ J