Theorem: MvPolynomial.homogenization_add_of_totalDegree_eq (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p q : MvPolynomial ι R
h : p.totalDegree = q.totalDegree
hpq : p.totalDegree = (p + q).totalDegree
⊢ homogenization i (p + q) = homogenization i p + homogenization i q
Tactic:
dsimp [homogenization]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p q : MvPolynomial ι R
h : p.totalDegree = q.totalDegree
hpq : p.totalDegree = (p + q).totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i ((p + q).totalDegree - j.sum fun x m => m)) (p + q) =
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p +
      Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m)) q

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p q : MvPolynomial ι R
h : p.totalDegree = q.totalDegree
hpq : p.totalDegree = (p + q).totalDegree
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i ((p + q).totalDegree - j.sum fun x m => m)) (p + q) =
    Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p +
      Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m)) q
Tactic:
rw [Finsupp.mapDomain_add, ← h, ← hpq]
State after:
no goals