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

State before:
σ : Type u_1
α : Type ?u.68078
inst✝ : Semiring α
f : MvPowerSeries σ α
x : σ
d : σ →₀ ℕ
⊢ d x ≤ degree d
Tactic:
convert le_weight _ x _ d
State after:
case convert_2
σ : Type u_1
α : Type ?u.68078
inst✝ : Semiring α
f : MvPowerSeries σ α
x : σ
d : σ →₀ ℕ
⊢ 1 ≠ 0

State before:
case convert_2
σ : Type u_1
α : Type ?u.68078
inst✝ : Semiring α
f : MvPowerSeries σ α
x : σ
d : σ →₀ ℕ
⊢ 1 ≠ 0
Tactic:
exact NeZero.ne 1
State after:
no goals