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

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ weightedOrder w f = ⊤ ↔ f = 0
Tactic:
constructor
State after:
case mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ weightedOrder w f = ⊤ → f = 0

case mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ f = 0 → weightedOrder w f = ⊤

State before:
case mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ weightedOrder w f = ⊤ → f = 0
Tactic:
intro h
State after:
case mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
⊢ f = 0

State before:
case mp
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
⊢ f = 0
Tactic:
ext d
State after:
case mp.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0

State before:
case mp.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0
Tactic:
rw [(coeff α d).map_zero, coeff_of_lt_weightedOrder w]
State after:
case mp.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ ↑((weight w) d) < weightedOrder w f

State before:
case mp.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ ↑((weight w) d) < weightedOrder w f
Tactic:
rw [h]
State after:
case mp.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ ↑((weight w) d) < ⊤

State before:
case mp.h.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : weightedOrder w f = ⊤
d : σ →₀ ℕ
⊢ ↑((weight w) d) < ⊤
Tactic:
exact WithTop.coe_lt_top _
State after:
no goals

State before:
case mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
⊢ f = 0 → weightedOrder w f = ⊤
Tactic:
rintro rfl
State after:
case mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ weightedOrder w 0 = ⊤

State before:
case mpr
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ weightedOrder w 0 = ⊤
Tactic:
exact weightedOrder_zero w
State after:
no goals