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

State before:
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
⊢ d x ≤ (weight w) d
Tactic:
simp only [weight_apply, Finsupp.sum]
State after:
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)

State before:
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
by_cases hxd : x ∈ d.support
State after:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)

case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∉ d.support
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)

State before:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∉ d.support
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
simp only [Finsupp.mem_support_iff, Classical.not_not] at hxd
State after:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : d x = 0
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)

State before:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : d x = 0
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
rw [hxd]
State after:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : d x = 0
⊢ 0 ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)

State before:
case neg
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : d x = 0
⊢ 0 ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
apply zero_le
State after:
no goals

State before:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ ∑ x ∈ d.support, Mul.mul (w x) (d x)
Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton hxd]
State after:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ Mul.mul (w x) (d x) + ∑ x ∈ d.support \ {x}, Mul.mul (w x) (d x)

State before:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ Mul.mul (w x) (d x) + ∑ x ∈ d.support \ {x}, Mul.mul (w x) (d x)
Tactic:
refine' le_trans _ (Nat.le_add_right _ _)
State after:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ Mul.mul (w x) (d x)

State before:
case pos
σ : Type u_1
α : Type ?u.2913
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
x : σ
hx : w x ≠ 0
d : σ →₀ ℕ
hxd : x ∈ d.support
⊢ d x ≤ Mul.mul (w x) (d x)
Tactic:
exact Nat.le_mul_of_pos_left _ (Nat.pos_of_ne_zero hx)
State after:
no goals