case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.307598
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0

case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.307598
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : ¬i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.307598
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
⊢ degreeOf i (X j) = if i = j then 1 else 0
by_cases c : i = j
no goals
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.307598
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : ¬i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0
simp [c, if_false, degreeOf_def, degrees_X]
no goals
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.307598
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝² : CommSemiring R
p q : MvPolynomial σ R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0
simp only [c, if_true, eq_self_iff_true, degreeOf_def, degrees_X, Multiset.count_singleton]