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

State before:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
⊢ {f | degree f ≤ n}.Finite
Tactic:
refine' finite_of_weight_le (Function.const σ 1) _ n
State after:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
⊢ ∀ (x : σ), Function.const σ 1 x ≠ 0

State before:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
⊢ ∀ (x : σ), Function.const σ 1 x ≠ 0
Tactic:
intro _
State after:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
x✝ : σ
⊢ Function.const σ 1 x✝ ≠ 0

State before:
σ : Type u_1
α : Type ?u.69196
inst✝¹ : Semiring α
f : MvPowerSeries σ α
inst✝ : Finite σ
n : ℕ
x✝ : σ
⊢ Function.const σ 1 x✝ ≠ 0
Tactic:
simp only [Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true]
State after:
no goals