internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same
Proof state before:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : (weightedDegree w) x = m
⊢ coeff x p = coeff x p

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = m
⊢ 0 = coeff x p
Tactic:
rfl
Proof state after:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = m
⊢ 0 = coeff x p
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = m
⊢ 0 = coeff x p
Tactic:
rw [zero_coeff]
Proof state after:
no goals
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weightedDegree w) x = m then coeff x p else 0) = coeff x p
Tactic:
rw [hp zero_coeff, if_pos]
Proof state after:
case neg.hc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ m = m
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same
Proof state before:
case neg.hc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ m = m
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
⊢ n ≠ m → (weightedHomogeneousComponent w n) p = 0
Tactic:
intro hn
Proof state after:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
⊢ (weightedHomogeneousComponent w n) p = 0
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
⊢ (weightedHomogeneousComponent w n) p = 0
Tactic:
ext x
Proof state after:
case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w n) p) = coeff x 0
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w n) p) = coeff x 0
Tactic:
rw [coeff_weightedHomogeneousComponent]
Proof state after:
case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
⊢ (if (weightedDegree w) x = n then coeff x p else 0) = coeff x 0
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
⊢ (if (weightedDegree w) x = n then coeff x p else 0) = coeff x 0
Tactic:
by_cases zero_coeff : coeff x p = 0
Proof state after:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weightedDegree w) x = n then coeff x p else 0) = coeff x 0

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weightedDegree w) x = n then coeff x p else 0) = coeff x 0
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weightedDegree w) x = n then coeff x p else 0) = coeff x 0
Tactic:
split_ifs
Proof state after:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : (weightedDegree w) x = n
⊢ coeff x p = coeff x 0

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = n
⊢ 0 = coeff x 0
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : (weightedDegree w) x = n
⊢ coeff x p = coeff x 0

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = n
⊢ 0 = coeff x 0
Tactic:
rw [zero_coeff]
Proof state after:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : (weightedDegree w) x = n
⊢ 0 = coeff x 0

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = n
⊢ 0 = coeff x 0
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : (weightedDegree w) x = n
⊢ 0 = coeff x 0

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = n
⊢ 0 = coeff x 0
Tactic:
rw [coeff_zero]
Proof state after:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = n
⊢ 0 = coeff x 0
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weightedDegree w) x = n
⊢ 0 = coeff x 0
Tactic:
rw [coeff_zero]
Proof state after:
no goals
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weightedDegree w) x = n then coeff x p else 0) = coeff x 0
Tactic:
rw [if_neg]
Proof state after:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ 0 = coeff x 0

case neg.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weightedDegree w) x = n
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ 0 = coeff x 0

case neg.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weightedDegree w) x = n
Tactic:
rw [coeff_zero]
Proof state after:
case neg.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weightedDegree w) x = n
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case neg.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weightedDegree w) x = n
Tactic:
rw [hp zero_coeff]
Proof state after:
case neg.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬m = n
Theorem: MvPolynomial.weightedHomogeneousComponent_of_weightedHomogeneous_ne
Proof state before:
case neg.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n✝ : M
φ ψ : MvPolynomial σ R
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬m = n
Tactic:
exact Ne.symm hn
Proof state after:
no goals
Theorem: MvPolynomial.DirectSum.coeLinearMap_eq_support_sum
Proof state before:
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)
⊢ (DirectSum.coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun x x_1 => ↑x_1
Tactic:
rw [DirectSum.coeLinearMap_eq_dfinsupp_sum]
Proof state after:
no goals
Theorem: MvPolynomial.DirectSum.coeLinearMap_eq_finsum
Proof state before:
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)
⊢ (DirectSum.coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)
Tactic:
rw [DirectSum.coeLinearMap_eq_support_sum, DFinsupp.sum]
Proof state after:
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)
⊢ ∑ i ∈ DFinsupp.support x, ↑(x i) = ∑ᶠ (m : M), ↑(x m)
Theorem: MvPolynomial.DirectSum.coeLinearMap_eq_finsum
Proof state before:
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)
⊢ ∑ i ∈ DFinsupp.support x, ↑(x i) = ∑ᶠ (m : M), ↑(x m)
Tactic:
rw [finsum_eq_sum_of_support_subset]
Proof state after:
case h
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)
⊢ (Function.support fun m => ↑(x m)) ⊆ ↑(DFinsupp.support x)
Theorem: MvPolynomial.DirectSum.coeLinearMap_eq_finsum
Proof state before:
case h
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)
⊢ (Function.support fun m => ↑(x m)) ⊆ ↑(DFinsupp.support x)
Tactic:
apply DirectSum.support_subset_submodule
Proof state after:
no goals
Theorem: MvPolynomial.weightedHomogeneousComponent_weightedHomogeneousPolynomial'
Proof state before:
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
m : M
x : ↥(weightedHomogeneousSubmodule R w m)
⊢ (weightedHomogeneousComponent w m) ↑x = ↑x
Tactic:
rw [weightedHomogeneousComponent_weighted_homogeneous_polynomial m m _ x.prop,
  if_pos rfl]
Proof state after:
no goals
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
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
⊢ (weightedHomogeneousComponent w m) ((DirectSum.coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x) = ↑(x m)
Tactic:
rw [DirectSum.coeLinearMap_eq_dfinsupp_sum, DFinsupp.sum, map_sum]
Proof state after:
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_1 ∈ DFinsupp.support x, (weightedHomogeneousComponent w m) ↑(x x_1) = ↑(x m)
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
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_1 ∈ DFinsupp.support x, (weightedHomogeneousComponent w m) ↑(x x_1) = ↑(x m)
Tactic:
convert @Finset.sum_eq_single M (MvPolynomial σ R) _ (DFinsupp.support x) _ m _ _
Proof state after:
case h.e'_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) = (weightedHomogeneousComponent w m) ↑(x m)

case convert_2
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
⊢ ∀ b ∈ DFinsupp.support x, b ≠ m → (weightedHomogeneousComponent w m) ↑(x b) = 0

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
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case h.e'_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) = (weightedHomogeneousComponent w m) ↑(x m)
Tactic:
rw [weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same]
Proof state after:
case h.e'_3.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 : M
⊢ IsWeightedHomogeneous w (↑(x m)) m
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case h.e'_3.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 : M
⊢ IsWeightedHomogeneous w (↑(x m)) m
Tactic:
rw [← mem_weightedHomogeneousSubmodule]
Proof state after:
case h.e'_3.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 : M
⊢ ↑(x m) ∈ weightedHomogeneousSubmodule R w m
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case h.e'_3.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 : M
⊢ ↑(x m) ∈ weightedHomogeneousSubmodule R w m
Tactic:
exact (x m).prop
Proof state after:
no goals
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case convert_2
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
⊢ ∀ b ∈ DFinsupp.support x, b ≠ m → (weightedHomogeneousComponent w m) ↑(x b) = 0
Tactic:
intro n _ hmn
Proof state after:
case convert_2
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
⊢ (weightedHomogeneousComponent w m) ↑(x n) = 0
Theorem: MvPolynomial.weightedHomogeneousComponent_directSum
Proof state before:
case convert_2
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
⊢ (weightedHomogeneousComponent w m) ↑(x n) = 0
Tactic:
rw [weightedHomogeneousComponent_of_weightedHomogeneous_ne n m]
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
⊢ 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