awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)
empty :
  ∀
    (h :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i → (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ ∅, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih :
      ∀ (h : ∀ i ∈ s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
        Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
          ((coeff d : (a : MvPowerSeries σ R) → R) f : R))
    (h : ∀ i ∈ Insert.insert a s, (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (g i)),
    Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ Insert.insert a s, (1 - g i)) : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_4 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * ∏ i ∈ s, (1 - g i)) : R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp only [Finset.prod_empty, mul_one]
  | insert a s ha ih =>
    simp only [Finset.mem_insert, forall_eq_or_imp] at h
    rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm,
      coeff_mul_left_one_sub_of_lt_weightedOrder w h.1, ih h.2]

Premises used: Finset.prod_empty, mul_assoc, Insert.insert, Finset.mem_insert, forall_eq_or_imp, mul_right_comm, mul_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f : MvPowerSeries σ R
by_contra! : ∀ (h : weightedOrder w (-f) ≠ weightedOrder w f), False
⊢ weightedOrder w (-f) = weightedOrder w f

Tactic:
by_contra! h
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f : MvPowerSeries σ R
h : weightedOrder w (-f) ≠ weightedOrder w f
⊢ f = 0

Tactic:
simpa using (weightedOrder_add_of_weightedOrder_ne w h).symm

Premises used: MvPowerSeries.weightedOrder_add_of_weightedOrder_ne, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f : MvPowerSeries σ R
h : weightedOrder w (-f) ≠ weightedOrder w f
⊢ f = 0

Tactic:
have : f = 0 := by simpa using (weightedOrder_add_of_weightedOrder_ne w h).symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
f : MvPowerSeries σ R
h : weightedOrder w (-f) ≠ weightedOrder w f
this : f = 0
⊢ False

Tactic:
simp [this] at h
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
⊢ weightedOrder w (p.toSubring T hp) = weightedOrder w p

Tactic:
eq_of_le_of_ge ?_ ?_

Premises used: eq_of_le_of_ge
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
refine_1 : weightedOrder w (p.toSubring T hp) ≤ weightedOrder w p
refine_2 : weightedOrder w p ≤ weightedOrder w (p.toSubring T hp)
⊢ weightedOrder w (p.toSubring T hp) = weightedOrder w p

Tactic:
refine eq_of_le_of_ge ?_ ?_

Premises used: eq_of_le_of_ge
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w (p.toSubring T hp)
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) p : R) (0 : R)

Tactic:
simp [coeff_eq_zero_of_lt_weightedOrder w hd, ← p.coeff_toSubring T hp]

Premises used: MvPowerSeries.coeff_toSubring, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
⊢ weightedOrder w (p.toSubring T hp) ≤ weightedOrder w p

Tactic:
refine le_weightedOrder w fun d hd => by
      simp [coeff_eq_zero_of_lt_weightedOrder w hd, ← p.coeff_toSubring T hp]

Premises used: MvPowerSeries.le_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w p
⊢ Eq.{u_3 + 1} (α := ↥T) ((coeff d : (a : MvPowerSeries σ ↥T) → ↥T) (p.toSubring T hp) : ↥T) (0 : ↥T)

Tactic:
exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_eq_zero_of_lt_weightedOrder w hd)
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), Membership.mem (α := R) T ((coeff n : (a : MvPowerSeries σ R) → R) p : R)
⊢ weightedOrder w p ≤ weightedOrder w (p.toSubring T hp)

Tactic:
refine le_weightedOrder w fun d hd => by
      exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_eq_zero_of_lt_weightedOrder w hd)

Premises used: MvPowerSeries.le_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
simp_rw :
  f ≠ 0 ↔
    ∃ (n : ℕ) (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n
⊢ f ≠ 0 ↔
    ∃ (n : ℕ) (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧ (degree : (a : σ →₀ ℕ) → ℕ) d = n

Tactic:
simp_rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔
    ∃ (n : ℕ) (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n

Tactic:
ne_zero_iff_exists_coeff_ne_zero_and_weight (fun _ => 1)

Premises used: MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔
    ∃ (n : ℕ) (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
        (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n

Tactic:
exact ne_zero_iff_exists_coeff_ne_zero_and_weight (fun _ => 1)

Premises used: MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
⊢ order.{u_1, u_2} (σ := σ) (R := R) 0 = ⊤

Tactic:
weightedOrder_zero _

Premises used: MvPowerSeries.weightedOrder_zero, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ (↑f.order.toNat : ℕ∞) = f.order

Tactic:
ne_zero_iff_weightedOrder_finite 1

Premises used: MvPowerSeries.ne_zero_iff_weightedOrder_finite, OfNat.ofNat, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
⊢ f.order = ⊤ ↔ f = 0

Tactic:
weightedOrder_eq_top_iff _

Premises used: MvPowerSeries.weightedOrder_eq_top_iff, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : (↑f.order.toNat : ℕ∞) = f.order
simp_rw :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = f.order
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = f.order

Tactic:
simp_rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : (↑f.order.toNat : ℕ∞) = f.order
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = f.order

Tactic:
exists_coeff_ne_zero_and_weightedOrder _ h

Premises used: MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : (↑f.order.toNat : ℕ∞) = f.order
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = f.order

Tactic:
exact exists_coeff_ne_zero_and_weightedOrder _ h

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
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
rw : f.order ≤ (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
⊢ f.order ≤ (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
rw [degree_eq_weight_one]

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

Tactic:
weightedOrder_le _ h

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

Tactic:
exact weightedOrder_le _ h

Premises used: MvPowerSeries.weightedOrder_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < f.order
⊢ (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < f.order

Tactic:
rw [degree_eq_weight_one] at h

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < f.order
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
coeff_eq_zero_of_lt_weightedOrder _ h

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < f.order
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
exact coeff_eq_zero_of_lt_weightedOrder _ h

Premises used: MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (degree : (a : σ →₀ ℕ) → ℕ) d < n → Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ ∀ (d : σ →₀ ℕ),
    (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d < n →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
simp_rw [degree_eq_weight_one] at h

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ
h :
  ∀ (d : σ →₀ ℕ),
    (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d < n →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ (↑n : ℕ∞) ≤ f.order

Tactic:
nat_le_weightedOrder _ h

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

Tactic:
exact nat_le_weightedOrder _ h

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

Tactic:
simp_rw [degree_eq_weight_one] at h

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h :
  ∀ (d : σ →₀ ℕ),
    (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < n →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ n ≤ f.order

Tactic:
le_weightedOrder _ h

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

Tactic:
exact le_weightedOrder _ h

Premises used: MvPowerSeries.le_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ
simp_rw :
  f.order = (↑n : ℕ∞) ↔
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ f.order = (↑n : ℕ∞) ↔
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (degree : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (degree : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
simp_rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ
⊢ f.order = (↑n : ℕ∞) ↔
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
weightedOrder_eq_nat _

Premises used: MvPowerSeries.weightedOrder_eq_nat, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ
⊢ f.order = (↑n : ℕ∞) ↔
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
          (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d = n) ∧
      ∀ (d : σ →₀ ℕ),
        (weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d < n →
          Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
exact weightedOrder_eq_nat _

Premises used: MvPowerSeries.weightedOrder_eq_nat
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
rw :
  order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
⊢ order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
⊢ order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
weightedOrder_monomial _

Premises used: MvPowerSeries.weightedOrder_monomial, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
⊢ order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
exact weightedOrder_monomial _

Premises used: MvPowerSeries.weightedOrder_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
d : σ →₀ ℕ
a : R
h : a ≠ 0
rw :
  order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
⊢ order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
rw [degree_eq_weight_one]

Premises used: Finsupp.degree_eq_weight_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
weightedOrder_monomial_of_ne_zero _ h

Premises used: MvPowerSeries.weightedOrder_monomial_of_ne_zero, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ order.{u_1, u_2} (σ := σ) (R := R) ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight fun (x : σ) ↦ 1 : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
exact weightedOrder_monomial_of_ne_zero _ h

Premises used: MvPowerSeries.weightedOrder_monomial_of_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f g : MvPowerSeries σ R
⊢ min f.order g.order ≤ (f + g).order

Tactic:
min_weightedOrder_le_add _

Premises used: MvPowerSeries.min_weightedOrder_le_add, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f g : MvPowerSeries σ R
h : f.order ≠ g.order
⊢ (f + g).order = min f.order g.order

Tactic:
weightedOrder_add_of_weightedOrder_ne _ h

Premises used: MvPowerSeries.weightedOrder_add_of_weightedOrder_ne, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f g : MvPowerSeries σ R
⊢ f.order + g.order ≤ (f * g).order

Tactic:
le_weightedOrder_mul _

Premises used: MvPowerSeries.le_weightedOrder_mul, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
n : ℕ
⊢ n • f.order ≤ (f ^ n).order

Tactic:
le_weightedOrder_pow _ n

Premises used: MvPowerSeries.le_weightedOrder_pow, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
f : ι → MvPowerSeries σ R
s : Finset ι
⊢ ∑ i ∈ s, (f i).order ≤ order.{u_1, u_3} (σ := σ) (R := R) (∏ i ∈ s, f i)

Tactic:
le_weightedOrder_prod _ _ _

Premises used: MvPowerSeries.le_weightedOrder_prod, MvPowerSeries.order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
mp : 1 ≤ f.order → Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
mpr : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R) → 1 ≤ f.order
⊢ 1 ≤ f.order ↔ Eq.{u_2 + 1} (α := R) ((constantCoeff : (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
f : MvPowerSeries σ R
h : 1 ≤ f.order
mp : (↑((degree : (a : σ →₀ ℕ) → ℕ) 0) : ℕ∞) < f.order
⊢ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
apply coeff_of_lt_order

Premises used: MvPowerSeries.coeff_of_lt_order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : 1 ≤ f.order
⊢ (↑((degree : (a : σ →₀ ℕ) → ℕ) 0) : ℕ∞) < f.order

Tactic:
simpa using Order.one_le_iff_pos.mp h

Premises used: Iff.mp, Order.one_le_iff_pos
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ 1 ≤ f.order

Tactic:
MvPowerSeries.le_order fun d hd ↦ ?_

Premises used: MvPowerSeries.le_order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
mpr :
  ∀ (d : σ →₀ ℕ) (hd : LT.lt (α := ℕ∞) (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) 1),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ 1 ≤ f.order

Tactic:
refine MvPowerSeries.le_order fun d hd ↦ ?_

Premises used: MvPowerSeries.le_order
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : LT.lt (α := ℕ∞) (↑((degree : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) 1
⊢ Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (0 : ℕ)

Tactic:
rw [Nat.cast_lt_one] at hd

Premises used: Nat.cast_lt_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
h : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
d : σ →₀ ℕ
hd : Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) (0 : ℕ)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
simp [(degree_eq_zero_iff d).mp hd, h]

Premises used: Iff.mp, Finsupp.degree_eq_zero_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
f : MvPowerSeries σ R
rw : 1 ≤ f.order ↔ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ↔
    Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ f.order ≠ 0 ↔ Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

Tactic:
rw [← ENat.one_le_iff_ne_zero, one_le_order_iff_constCoeff_eq_zero]

Premises used: MvPowerSeries.one_le_order_iff_constCoeff_eq_zero, ENat.one_le_iff_ne_zero