Theorem: MvPowerSeries.weight_apply (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

State before:
σ : Type u_1
α : Type ?u.2439
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (weight w) d = d.sum fun x => Mul.mul (w x)
Tactic:
simp only [weight]
State after:
σ : Type u_1
α : Type ?u.2439
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ { toFun := fun d => d.sum fun x y => w x * y, map_zero' := ⋯, map_add' := ⋯ } d = d.sum fun x => Mul.mul (w x)

State before:
σ : Type u_1
α : Type ?u.2439
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ { toFun := fun d => d.sum fun x y => w x * y, map_zero' := ⋯, map_add' := ⋯ } d = d.sum fun x => Mul.mul (w x)
Tactic:
rfl
State after:
no goals