erw [Finsupp.mapDomain_single, Finsupp.mapDomain_single]
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.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n)) +
      Finsupp.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (C 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
⊢ 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