rw [← C_mul_X_pow_eq_monomial]
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = ((monomial (Finsupp.single j n)) 1 + C r).totalDegree
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = (C 1 * X j ^ n + C r).totalDegree