σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
⊢ ↑(homogeneousComponent m) p = if m = n then p else 0
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : p ∈ homogeneousSubmodule σ R n
⊢ ↑(homogeneousComponent m) p = if m = n then p else 0
simp only [mem_homogeneousSubmodule] at h
case a
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
⊢ coeff x (↑(homogeneousComponent m) p) = coeff x (if m = n then p else 0)
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
⊢ ↑(homogeneousComponent m) p = if m = n then p else 0
ext x
case a
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
⊢ (if ∑ i in x.support, ↑x i = m then coeff x p else 0) = coeff x (if m = n then p else 0)
case a
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
⊢ coeff x (↑(homogeneousComponent m) p) = coeff x (if m = n then p else 0)
rw [coeff_homogeneousComponent]
case pos
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if ∑ i in x.support, ↑x i = m then coeff x p else 0) = coeff x (if m = n then p else 0)

case neg
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if ∑ i in x.support, ↑x i = m then coeff x p else 0) = coeff x (if m = n then p else 0)
case a
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
⊢ (if ∑ i in x.support, ↑x i = m then coeff x p else 0) = coeff x (if m = n then p else 0)
by_cases zero_coeff : coeff x p = 0
case pos.inl.inl
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ∑ i in x.support, ↑x i = m
h✝ : m = n
⊢ coeff x p = coeff x p

case pos.inl.inr
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ∑ i in x.support, ↑x i = m
h✝ : ¬m = n
⊢ coeff x p = coeff x 0

case pos.inr.inl
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬∑ i in x.support, ↑x i = m
h✝ : m = n
⊢ 0 = coeff x p

case pos.inr.inr
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬∑ i in x.support, ↑x i = m
h✝ : ¬m = n
⊢ 0 = coeff x 0
case pos
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if ∑ i in x.support, ↑x i = m then coeff x p else 0) = coeff x (if m = n then p else 0)
split_ifs
no goals
case pos.inl.inl
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ∑ i in x.support, ↑x i = m
h✝ : m = n
⊢ coeff x p = coeff x p

case pos.inl.inr
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ∑ i in x.support, ↑x i = m
h✝ : ¬m = n
⊢ coeff x p = coeff x 0

case pos.inr.inl
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬∑ i in x.support, ↑x i = m
h✝ : m = n
⊢ 0 = coeff x p

case pos.inr.inr
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬∑ i in x.support, ↑x i = m
h✝ : ¬m = n
⊢ 0 = coeff x 0
all_goals simp only [zero_coeff, coeff_zero]
no goals
case pos.inr.inr
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝¹ : ¬∑ i in x.support, ↑x i = m
h✝ : ¬m = n
⊢ 0 = coeff x 0
simp only [zero_coeff, coeff_zero]
case neg
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if n = m then coeff x p else 0) = coeff x (if m = n then p else 0)
case neg
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if ∑ i in x.support, ↑x i = m then coeff x p else 0) = coeff x (if m = n then p else 0)
rw [h zero_coeff]
case neg
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if m = n then coeff x p else 0) = coeff x (if m = n then p else 0)
case neg
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if n = m then coeff x p else 0) = coeff x (if m = n then p else 0)
simp only [show n = m ↔ m = n from eq_comm]
case neg.inl
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
h1 : m = n
⊢ coeff x p = coeff x p

case neg.inr
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
h1 : ¬m = n
⊢ 0 = coeff x 0
case neg
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if m = n then coeff x p else 0) = coeff x (if m = n then p else 0)
split_ifs with h1
no goals
case neg.inl
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
h1 : m = n
⊢ coeff x p = coeff x p
rfl
no goals
case neg.inr
σ : Type u_1
τ : Type ?u.368740
R : Type u_2
S : Type ?u.368746
inst✝ : CommSemiring R
n✝ : ℕ
φ ψ : MvPolynomial σ R
m n : ℕ
p : MvPolynomial σ R
h : IsHomogeneous p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
h1 : ¬m = n
⊢ 0 = coeff x 0
simp only [coeff_zero]