awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
simp_rw :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
        (if x : f = 0 then ⊤
        else
          (↑(Nat.find (p := fun (n : ℕ) ↦
                ∃ (d : σ →₀ ℕ),
                  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                    (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
                ⋯) :
            ℕ∞))
simp_rw₁ :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
        (↑(Nat.find (p := fun (n : ℕ) ↦
              ∃ (d : σ →₀ ℕ),
                Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                  (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
              ⋯) :
          ℕ∞)
simp_rw₂ :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (weight w : (a : σ →₀ ℕ) → ℕ) d =
        Nat.find (p := fun (n : ℕ) ↦
          ∃ (d : σ →₀ ℕ),
            Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
              (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
          ⋯
simp_rw₃ :
  ∀
    (h1 :
      ∃ (n : ℕ) (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight w : (a : σ →₀ ℕ) → ℕ) d = n),
    ∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d =
          Nat.find (p := fun (n : ℕ) ↦
            ∃ (d : σ →₀ ℕ),
              Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
                (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
            h1
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f

Tactic:
classical
  simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]
  generalize_proofs h1
  exact Nat.find_spec h1

Premises used: Iff.mpr, MvPowerSeries.ne_zero_iff_weightedOrder_finite, Nat.cast_inj, dif_neg, MvPowerSeries.weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
rw :
  LE.le (α := ℕ∞)
    (↑(Nat.find (p := fun (n : ℕ) ↦
          ∃ (d : σ →₀ ℕ),
            Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
              (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
          ⋯) :
      ℕ∞)
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
hnc : ¬f = 0
⊢ weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
rw [weightedOrder, dif_neg]

Premises used: dif_neg, MvPowerSeries.weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
simp :
  ∃ m ≤ (weight w : (a : σ →₀ ℕ) → ℕ) d,
    ∃ (d : σ →₀ ℕ),
      ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = m
⊢ LE.le (α := ℕ∞)
    (↑(Nat.find (p := fun (n : ℕ) ↦
          ∃ (d : σ →₀ ℕ),
            Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
              (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
          ⋯) :
      ℕ∞)
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]

Premises used: ne_eq, Nat.find_le_iff, Nat.cast_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ ∃ m ≤ (weight w : (a : σ →₀ ℕ) → ℕ) d,
    ∃ (d : σ →₀ ℕ),
      ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = m

Tactic:
⟨weight w d, le_rfl, d, h, rfl⟩

Premises used: le_rfl, Finsupp.weight, And.intro, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ ∃ m ≤ (weight w : (a : σ →₀ ℕ) → ℕ) d,
    ∃ (d : σ →₀ ℕ),
      ¬Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = m

Tactic:
exact ⟨weight w d, le_rfl, d, h, rfl⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ ¬f = 0

Tactic:
(f.ne_zero_iff_exists_coeff_ne_zero_and_weight w).mpr ⟨weight w d, d, h, rfl⟩

Premises used: Iff.mpr, Finsupp.weight, And.intro, Exists.intro, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ ¬f = 0

Tactic:
exact (f.ne_zero_iff_exists_coeff_ne_zero_and_weight w).mpr ⟨weight w d, d, h, rfl⟩

Premises used: Iff.mpr, Finsupp.weight, And.intro, Exists.intro, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f
contrapose! :
  ∀ (h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
weightedOrder_le w h

Premises used: MvPowerSeries.weightedOrder_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
exact weightedOrder_le w h

Premises used: MvPowerSeries.weightedOrder_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
by_contra! : ∀ (H : weightedOrder w f < (↑n : ℕ∞)), False
⊢ (↑n : ℕ∞) ≤ weightedOrder w f

Tactic:
by_contra! H
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
rw : weightedOrder w f ≠ ⊤
⊢ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f

Tactic:
rw [coe_toNat_eq_self]

Premises used: ENat.coe_toNat_eq_self
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
⊢ weightedOrder w f ≠ ⊤

Tactic:
ne_top_of_lt H

Premises used: ne_top_of_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
⊢ weightedOrder w f ≠ ⊤

Tactic:
exact ne_top_of_lt H

Premises used: ne_top_of_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
⊢ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f

Tactic:
have : (f.weightedOrder w).toNat = f.weightedOrder w := by
    rw [coe_toNat_eq_self]; exact ne_top_of_lt H
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
this : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
obtain :
  ∀ (d : σ →₀ ℕ) (hfd : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R))
    (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f), False
⊢ False

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

Premises used: MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
this : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hfd : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
⊢ (weight w : (a : σ →₀ ℕ) → ℕ) d < n

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

Premises used: Nat.cast_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
this : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hfd : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
H₁ : (weight w : (a : σ →₀ ℕ) → ℕ) d < n
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

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

Premises used: Nat.cast_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
H : weightedOrder w f < (↑n : ℕ∞)
this : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hfd : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
H₁ : (weight w : (a : σ →₀ ℕ) → ℕ) d < n
hfd₁ : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f

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

Premises used: Nat.cast_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
this : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
H : (weight w : (a : σ →₀ ℕ) → ℕ) d < n
hfd : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
⊢ False

Tactic:
hfd (h d H)
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
this : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
H : (weight w : (a : σ →₀ ℕ) → ℕ) d < n
hfd : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
⊢ False

Tactic:
exact hfd (h d H)
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ∞
h :
  ∀ (d : σ →₀ ℕ),
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < n →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
top :
  ∀
    (h :
      ∀ (d : σ →₀ ℕ),
        LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) ⊤ →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    ⊤ ≤ weightedOrder w f
coe :
  ∀ (a : ℕ)
    (h :
      ∀ (d : σ →₀ ℕ),
        LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) (↑a : ℕ∞) →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)),
    (↑a : ℕ∞) ≤ weightedOrder w f
⊢ n ≤ weightedOrder w f

Tactic:
cases n
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) ⊤ →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
top : f = 0
⊢ ⊤ ≤ weightedOrder w f

Tactic:
rw [top_le_iff, weightedOrder_eq_top_iff]

Premises used: top_le_iff, MvPowerSeries.weightedOrder_eq_top_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) ⊤ →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
top :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ f = 0

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) ⊤ →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
h d (ENat.coe_lt_top _)

Premises used: ENat.coe_lt_top
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h :
  ∀ (d : σ →₀ ℕ),
    LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) ⊤ →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
exact h d (ENat.coe_lt_top _)

Premises used: ENat.coe_lt_top
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) (↑a : ℕ∞) →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
coe :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < a → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (↑a : ℕ∞) ≤ weightedOrder w f

Tactic:
apply nat_le_weightedOrder

Premises used: MvPowerSeries.nat_le_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    LT.lt (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) (↑a : ℕ∞) →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < a → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
simpa only [ENat.some_eq_coe, Nat.cast_lt] using h

Premises used: ENat.some_eq_coe, Nat.cast_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
mp :
  weightedOrder w f = (↑n : ℕ∞) →
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
mpr :
  ((∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)) →
    weightedOrder w f = (↑n : ℕ∞)
⊢ weightedOrder w f = (↑n : ℕ∞) ↔
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : 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]

Premises used: ENat.toNat_coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = (↑n : ℕ∞)
mp :
  ∀ (d : σ →₀ ℕ)
    (hd :
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f),
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
    ∀ (d : σ →₀ ℕ),
      (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

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

Premises used: MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = (↑n : ℕ∞)
d : σ →₀ ℕ
hd :
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (weight w : (a : σ →₀ ℕ) → ℕ) d = n

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

Premises used: Nat.cast_inj, ne_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = (↑n : ℕ∞)
d : σ →₀ ℕ
hd :
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
e : σ →₀ ℕ
he : (weight w : (a : σ →₀ ℕ) → ℕ) e < n
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) e) : ℕ∞) < weightedOrder w f

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

Premises used: Nat.cast_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : weightedOrder w f = (↑n : ℕ∞)
d : σ →₀ ℕ
hd :
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f
⊢ (∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight w : (a : σ →₀ ℕ) → ℕ) d = n) ∧
    ∀ (d : σ →₀ ℕ),
      (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

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])⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
⊢ weightedOrder w f = (↑n : ℕ∞)

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

Premises used: MvPowerSeries.nat_le_weightedOrder, le_antisymm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
⊢ weightedOrder w f = (↑n : ℕ∞)

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

Premises used: MvPowerSeries.nat_le_weightedOrder, le_antisymm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
pos : ∀ (h : a = 0), weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) = ⊤
neg :
  ∀ (h : ¬a = 0),
    weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
      (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
h : a = 0
pos : weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) 0) = ⊤
pos₁ : Eq (α := MvPowerSeries σ R) ((monomial d : (a : R) → MvPowerSeries σ R) 0) 0
pos₂ pos₃ : Eq (α := MvPowerSeries σ R) 0 0
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) = ⊤

Tactic:
rw [h, weightedOrder_eq_top_iff, map_zero]

Premises used: map_zero, MvPowerSeries.weightedOrder_eq_top_iff