congr
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
case e_a.e_a.e_s
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 j n + (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n) =
    Finsupp.single j n

case e_a
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 i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r = C r * X i ^ n