-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem nat_le_weightedOrder {n : ℕ} (h : ∀ d, weight w d < n → coeff R d f = 0) :
    n ≤ f.weightedOrder w

Proof state:
case intro.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hfd : (coeff R d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False

Tactic:
exact hfd (h d H)

Result:
no goals

Proof state:
case intro.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
H : weightedOrder w f < ↑n
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
hfd : (coeff R d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False

Tactic:
rw [← hd, Nat.cast_lt] at H

Result:
case intro.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
H : (weight w) d < n
hfd : (coeff R d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
⊢ ↑n ≤ weightedOrder w f

Tactic:
by_contra! H

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
H : weightedOrder w f < ↑n
⊢ False

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
H : weightedOrder w f < ↑n
this : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ False

Tactic:
obtain ⟨d, hfd, hd⟩ := exists_coeff_ne_zero_and_weightedOrder w this

Result:
case intro.intro
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
H : weightedOrder w f < ↑n
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
hfd : (coeff R d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
H : weightedOrder w f < ↑n
⊢ weightedOrder w f ≠ ⊤

Tactic:
exact ne_top_of_lt H

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
H : weightedOrder w f < ↑n
⊢ False

Tactic:
have : (f.weightedOrder w).toNat = f.weightedOrder w := by
  rw [coe_toNat_eq_self]; exact ne_top_of_lt H

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
H : weightedOrder w f < ↑n
this : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ False

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
H : weightedOrder w f < ↑n
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
rw [coe_toNat_eq_self]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0
H : weightedOrder w f < ↑n
⊢ weightedOrder w f ≠ ⊤