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

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:
rw [weightedOrder, dif_neg]
State after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)

case hnc
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ¬f = 0

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)
Tactic:
simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]
State after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ∃ m ≤ (weight w) d, ∃ d, (weight w) d = m ∧ ¬(coeff α d) f = 0

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ∃ m ≤ (weight w) d, ∃ d, (weight w) d = m ∧ ¬(coeff α d) f = 0
Tactic:
exact ⟨weight w d, le_rfl, d, rfl, h⟩
State after:
no goals

State before:
case hnc
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
h : (coeff α d) f ≠ 0
⊢ ¬f = 0
Tactic:
exact (f.exists_coeff_ne_zero_of_weight_iff_ne_zero w).mp ⟨weight w d, d, rfl, h⟩
State after:
no goals