simp only [tsub_zero, Finsupp.sum_zero_index, Finsupp.sum_single_index, zero_add,
  single_eq_monomial, one_pow, mul_one, Finsupp.smul_single', Finsupp.single_tsub]
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
⊢ Finsupp.single
        (n • Finsupp.single j 1 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree -
              (n • Finsupp.single j 1).sum fun x m => m))
        (1 ^ n) +
      Finsupp.single
        (0 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - Finsupp.sum 0 fun x m => m))
        r =
    AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r * X i ^ n
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
⊢ (monomial
          (Finsupp.single j n +
            (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n)))
        1 +
      (monomial (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r =
    (monomial (Finsupp.single j n)) 1 + C r * X i ^ n