Theorem: MvPolynomial.weightedHomogeneousComponent_of_weighted_homogeneous_polynomial_same (DividedPowers/ForMathlib/WeightedHomogeneous.lean)

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 : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
⊢ (weightedHomogeneousComponent w m) p = p
Tactic:
ext x
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 : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m) p) = coeff x p

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 : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m) p) = coeff x p
Tactic:
rw [coeff_weightedHomogeneousComponent]
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 : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ (if (weightedDegree w) x = m then coeff x p else 0) = coeff x p

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 : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ (if (weightedDegree w) x = m then coeff x p else 0) = coeff x p
Tactic:
by_cases zero_coeff : coeff x p = 0
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 : 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

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

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
⊢ (if (weightedDegree w) x = m then coeff x p else 0) = coeff x p
Tactic:
split_ifs
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 : 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

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
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

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]
State after:
no goals

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]
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

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
State after:
no goals