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

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
⊢ min (weightedOrder w f) (weightedOrder w g) ≤ weightedOrder w (f + g)
Tactic:
refine' le_weightedOrder w _
State after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
⊢ ∀ (d : σ →₀ ℕ), ↑((weight w) d) < min (weightedOrder w f) (weightedOrder w g) → (coeff α d) (f + g) = 0

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f g : MvPowerSeries σ α
⊢ ∀ (d : σ →₀ ℕ), ↑((weight w) d) < min (weightedOrder w f) (weightedOrder w g) → (coeff α d) (f + g) = 0
Tactic:
simp (config := { contextual := true }) only [coeff_of_lt_weightedOrder w, lt_min_iff, map_add,
  add_zero, eq_self_iff_true, imp_true_iff]
State after:
no goals