simp only [tsub_zero, Finsupp.sum_zero_index, Finsupp.sum_single_index, this, add_zero,
  Finsupp.single_zero, zero_add, single_eq_monomial]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ Finsupp.single
        (Finsupp.single j 1 + Finsupp.single i ((X j + C r).totalDegree - (Finsupp.single j 1).sum fun x m => m)) 1 +
      Finsupp.single (0 + Finsupp.single i ((X j + C r).totalDegree - Finsupp.sum 0 fun x m => m)) r =
    X j + C r * X i
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ (monomial (Finsupp.single j 1 + Finsupp.single i (1 - 1))) 1 + (monomial (Finsupp.single i 1)) r = X j + C r * X i