erw [homogenization, Finsupp.mapDomain_add, Finsupp.mapDomain_single, Finsupp.mapDomain_single]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ homogenization i (X j + C 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
⊢ 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