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

State before:
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ degree d = d.sum fun x => id
Tactic:
rw [degree, weight_apply]
State after:
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (d.sum fun x => Mul.mul 1) = d.sum fun x => id

State before:
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (d.sum fun x => Mul.mul 1) = d.sum fun x => id
Tactic:
apply congr_arg
State after:
case h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (fun x => Mul.mul 1) = fun x => id

State before:
case h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (fun x => Mul.mul 1) = fun x => id
Tactic:
ext _ n
State after:
case h.h.h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
⊢ Mul.mul 1 n = id n

State before:
case h.h.h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
⊢ Mul.mul 1 n = id n
Tactic:
have h_eq : Mul.mul 1 n = 1 * n := by rfl
State after:
case h.h.h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
h_eq : Mul.mul 1 n = 1 * n
⊢ Mul.mul 1 n = id n

State before:
case h.h.h
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
h_eq : Mul.mul 1 n = 1 * n
⊢ Mul.mul 1 n = id n
Tactic:
rw [h_eq, id_eq, one_mul]
State after:
no goals

State before:
σ : Type u_1
α : Type ?u.65991
inst✝ : Semiring α
f : MvPowerSeries σ α
d : σ →₀ ℕ
x✝ : σ
n : ℕ
⊢ Mul.mul 1 n = 1 * n
Tactic:
rfl
State after:
no goals