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

State before:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < n → (coeff α d) f = 0
⊢ n ≤ weightedOrder w f
Tactic:
cases n
State after:
case top
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff α d) f = 0
⊢ ⊤ ≤ weightedOrder w f

case coe
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff α d) f = 0
⊢ ↑a✝ ≤ weightedOrder w f

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

State before:
case top
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff α d) f = 0
⊢ f = 0
Tactic:
ext d
State after:
case top.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ⊤ → (coeff α d) f = 0
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0

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

State before:
case coe
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff α d) f = 0
⊢ ↑a✝ ≤ weightedOrder w f
Tactic:
apply nat_le_weightedOrder
State after:
case coe.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff α d) f = 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < a✝ → (coeff α d) f = 0

State before:
case coe.h
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
a✝ : ℕ
h : ∀ (d : σ →₀ ℕ), ↑((weight w) d) < ↑a✝ → (coeff α d) f = 0
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < a✝ → (coeff α d) f = 0
Tactic:
simpa only [ENat.some_eq_coe, Nat.cast_lt] using h
State after:
no goals