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

State before:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ φ.totalDegree = weightedTotalDegree 1 φ
Tactic:
rw [totalDegree, weightedTotalDegree, weightedDegree]
State after:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ (φ.support.sup fun s => s.sum fun x e => e) = φ.support.sup fun s => (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom s

State before:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ (φ.support.sup fun s => s.sum fun x e => e) = φ.support.sup fun s => (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom s
Tactic:
apply Finset.sup_congr rfl
State after:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ ∀ a ∈ φ.support, (a.sum fun x e => e) = (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom a

State before:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ ∀ a ∈ φ.support, (a.sum fun x e => e) = (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom a
Tactic:
intro a _
State after:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
a : σ →₀ ℕ
a✝ : a ∈ φ.support
⊢ (a.sum fun x e => e) = (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom a

State before:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
a : σ →₀ ℕ
a✝ : a ∈ φ.support
⊢ (a.sum fun x e => e) = (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom a
Tactic:
simp only [Finsupp.total, Pi.one_apply, LinearMap.toAddMonoidHom_coe, Finsupp.coe_lsum,
  LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, Algebra.id.smul_eq_mul, mul_one]
State after:
no goals