Theorem: MvPolynomial.IsHomogeneous.totalDegree (DividedPowers/ForMathlib/Homogeneous.lean)

State before:
σ : Type u_1
τ : Type ?u.36379
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.36388
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
⊢ φ.totalDegree = n
Tactic:
rw [totalDegree_eq_weightedTotalDegree, ← WithBot.coe_eq_coe, ←
  weightedTotalDegree_coe _ φ h, IsWeightedHomogeneous.weighted_total_degree hφ h]
State after:
no goals