-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem weightedOrder_eq_nat {n : ℕ} :
    f.weightedOrder w = n ↔
      (∃ d, coeff R d f ≠ 0 ∧ weight w d = n) ∧ ∀ d, weight w d < n → coeff R d f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = ↑n
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
simp only [h, toNat_coe]

Result:
no goals

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

Tactic:
intro h

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

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

Tactic:
simpa [h, Nat.cast_inj, ne_eq] using hd

Result:
no goals

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

Tactic:
constructor

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

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ ((∃ d, (coeff R d) f ≠ 0 ∧ (weight w) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff R d) f = 0) →
    weightedOrder w f = ↑n

Proof state:
case mpr.intro.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
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ weightedOrder w f = ↑n

Tactic:
exact le_antisymm (hd.symm ▸ f.weightedOrder_le w hd') (nat_le_weightedOrder w h)

Result:
no goals

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

Tactic:
rintro ⟨⟨d, hd', hd⟩, h⟩

Result:
case mpr.intro.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
d : σ →₀ ℕ
hd' : (coeff R d) f ≠ 0
hd : (weight w) d = n
⊢ weightedOrder w f = ↑n

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

Tactic:
obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by simp only [h, toNat_coe])

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

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = ↑n
d : σ →₀ ℕ
hd : (coeff R d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f
e : σ →₀ ℕ
he : (weight w) e < n
⊢ ↑((weight w) e) < weightedOrder w f

Tactic:
simp only [h, Nat.cast_lt, he]

Result:
no goals

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

Tactic:
exact ⟨⟨d, by simpa [h, Nat.cast_inj, ne_eq] using hd⟩,
  fun e he ↦ f.coeff_eq_zero_of_lt_weightedOrder w (by simp only [h, Nat.cast_lt, he])⟩

Result:
no goals