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

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w f
⊢ (coeff α d) f = 0
Tactic:
contrapose! h
State after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)
Tactic:
exact weightedOrder_le w f h
State after:
no goals