Theorem: MvPolynomial.totalDegree_eq_weightedTotalDegree (DividedPowers/ForMathlib/Homogeneous.lean)

State before:
σ : Type u_2
τ : Type ?u.7209
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.7218
φ : MvPolynomial σ R
⊢ φ.totalDegree = weightedTotalDegree 1 φ
Tactic:
simp only [totalDegree, weightedTotalDegree, weightedDegree, LinearMap.toAddMonoidHom_coe,
  Finsupp.total, Pi.one_apply, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe,
  id_eq, Algebra.id.smul_eq_mul, mul_one]
State after:
no goals