Theorem: MvPowerSeries.nat_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:
by_contra H
State after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : ¬↑n ≤ weightedOrder w f
⊢ False

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
H : ¬↑n ≤ weightedOrder w f
⊢ False
Tactic:
rw [not_le] at H
State after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
⊢ False

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
H : weightedOrder w f < ↑n
⊢ False
Tactic:
have : ↑(toNat (f.weightedOrder w)) = f.weightedOrder w := by
  rw [coe_toNat_eq_self] ; exact ne_top_of_lt H
State after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ False

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
H : weightedOrder w f < ↑n
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
⊢ False
Tactic:
obtain ⟨d, hd, hfd⟩ := exists_coeff_ne_zero_of_weightedOrder w f this
State after:
case intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w f
hfd : (coeff α d) f ≠ 0
⊢ False

State before:
case intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
d : σ →₀ ℕ
hd : ↑((weight w) d) = weightedOrder w f
hfd : (coeff α d) f ≠ 0
⊢ False
Tactic:
rw [← hd, Nat.cast_lt] at H
State after:
case intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hd : ↑((weight w) d) = weightedOrder w f
hfd : (coeff α d) f ≠ 0
⊢ False

State before:
case intro.intro
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
this : ↑(toNat (weightedOrder w f)) = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hd : ↑((weight w) d) = weightedOrder w f
hfd : (coeff α d) f ≠ 0
⊢ False
Tactic:
exact hfd (h d H)
State after:
no goals

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
H : weightedOrder w f < ↑n
⊢ ↑(toNat (weightedOrder w f)) = weightedOrder w f
Tactic:
rw [coe_toNat_eq_self]
State after:
σ : Type u_2
α : Type u_1
inst✝ : Semiring α
w : σ → ℕ
f✝ f : MvPowerSeries σ α
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff α d) f = 0
H : weightedOrder w f < ↑n
⊢ weightedOrder w f ≠ ⊤

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
H : weightedOrder w f < ↑n
⊢ weightedOrder w f ≠ ⊤
Tactic:
exact ne_top_of_lt H
State after:
no goals