awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
inl : (↑p : ℕ∞) = weightedOrder w f
⊢ False

Tactic:
refine weightedHomogeneousComponent_of_weightedOrder ?_ H

Premises used: MvPowerSeries.weightedHomogeneousComponent_of_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
inl : ¬f = 0
⊢ (↑p : ℕ∞) = weightedOrder w f

Tactic:
simp only [ENat.coe_toNat_eq_self, ne_eq, weightedOrder_eq_top_iff, p, q]

Premises used: ne_eq, ENat.coe_toNat_eq_self, MvPowerSeries.weightedOrder_eq_top_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
inl : (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
⊢ ¬f = 0

Tactic:
rw [← ne_eq, ne_zero_iff_weightedOrder_finite w]

Premises used: MvPowerSeries.ne_zero_iff_weightedOrder_finite, ne_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
⊢ weightedOrder w f < ⊤

Tactic:
simpa
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
⊢ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f

Tactic:
exact ENat.coe_toNat (ne_top_of_lt (by simpa))

Premises used: ENat.coe_toNat, ne_top_of_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
⊢ False

Tactic:
weightedHomogeneousComponent_of_weightedOrder ?_ H

Premises used: MvPowerSeries.weightedHomogeneousComponent_of_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
inr : (↑q : ℕ∞) = weightedOrder w g
⊢ False

Tactic:
refine weightedHomogeneousComponent_of_weightedOrder ?_ H

Premises used: MvPowerSeries.weightedHomogeneousComponent_of_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
inr : ¬g = 0
⊢ (↑q : ℕ∞) = weightedOrder w g

Tactic:
simp only [ENat.coe_toNat_eq_self, ne_eq, weightedOrder_eq_top_iff, p, q]

Premises used: ne_eq, ENat.coe_toNat_eq_self, MvPowerSeries.weightedOrder_eq_top_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
inr : (↑(weightedOrder w g).toNat : ℕ∞) = weightedOrder w g
⊢ ¬g = 0

Tactic:
rw [← ne_eq, ne_zero_iff_weightedOrder_finite w]

Premises used: MvPowerSeries.ne_zero_iff_weightedOrder_finite, ne_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
⊢ weightedOrder w g < ⊤

Tactic:
simpa
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
H :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
⊢ (↑(weightedOrder w g).toNat : ℕ∞) = weightedOrder w g

Tactic:
exact ENat.coe_toNat (ne_top_of_lt (by simpa))

Premises used: ENat.coe_toNat, ne_top_of_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
⊢ HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
      ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R) ≠
    0

Tactic:
have : f.weightedHomogeneousComponent w p * g.weightedHomogeneousComponent w q ≠ 0 := by
        simp only [ne_eq, mul_eq_zero]
        intro H
        rcases H with H | H <;>
        · refine weightedHomogeneousComponent_of_weightedOrder ?_ H
          simp only [ENat.coe_toNat_eq_self, ne_eq, weightedOrder_eq_top_iff, p, q]
          rw [← ne_eq, ne_zero_iff_weightedOrder_finite w]
          exact ENat.coe_toNat (ne_top_of_lt (by simpa))
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
this :
  HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
      ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R) ≠
    0
⊢ Ne (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)

Tactic:
rw [← weightedHomogeneousComponent_mul_of_le_weightedOrder
          (le_of_eq hp) (le_of_eq hq)] at this

Premises used: MvPowerSeries.weightedHomogeneousComponent_mul_of_le_weightedOrder, le_of_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
this :
  Ne (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
pos : ¬(↑(p + q) : ℕ∞) < weightedOrder w (f * g)
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

Tactic:
rw [← hp, ← hq, ← Nat.cast_add, ← not_lt]

Premises used: Nat.cast_add, not_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
this :
  Ne (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
H : (↑(p + q) : ℕ∞) < weightedOrder w (f * g)
pos :
  Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
⊢ False

Tactic:
apply this
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
this :
  Ne (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
H : (↑(p + q) : ℕ∞) < weightedOrder w (f * g)
⊢ Eq (α := MvPowerSeries σ R)
    ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)

Tactic:
apply weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero H

Premises used: MvPowerSeries.weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : ¬weightedOrder w g < ⊤
⊢ weightedOrder w g = ⊤

Tactic:
rw [not_lt_top_iff] at hg

Premises used: not_lt_top_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g = ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

Tactic:
simp [hg]
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : ¬weightedOrder w f < ⊤
⊢ weightedOrder w f = ⊤

Tactic:
rw [not_lt_top_iff] at hf

Premises used: not_lt_top_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f = ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

Tactic:
simp [hf]
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
⊢ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, weightedOrder w (f i)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i) = ∑ i ∈ s, weightedOrder w (f i)
cons :
  weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i) =
    weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x)
cons₁ : weightedOrder w (f a * ∏ x ∈ s, f x) = weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x)
cons₂ :
  weightedOrder w (f a) + weightedOrder.{u_1, u_3} (R := R) w (∏ x ∈ s, f x) =
    weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x)
cons₃ cons₄ :
  weightedOrder w (f a) + ∑ i ∈ s, weightedOrder w (f i) = weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x)
⊢ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i) = ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i)

Tactic:
rw [Finset.sum_cons ha, Finset.prod_cons ha, weightedOrder_mul, ih]

Premises used: Finset.sum_cons, MvPowerSeries.weightedOrder_mul, Finset.prod_cons
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
s : Finset ι
empty : weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, weightedOrder w (f i)
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih : weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i) = ∑ i ∈ s, weightedOrder w (f i)),
    weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i) =
      ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i)
⊢ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i) = ∑ i ∈ s, weightedOrder w (f i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih => rw [Finset.sum_cons ha, Finset.prod_cons ha, weightedOrder_mul, ih]

Premises used: MvPowerSeries.weightedOrder_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
f g : MvPowerSeries σ R
⊢ (f * g).order = f.order + g.order

Tactic:
weightedOrder_mul _ f g

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

Tactic:
weightedOrder_prod _ _ _

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

Tactic:
simpa using ne_zero_iff_exists_coeff_ne_zero f

Premises used: MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f_1 g f : MvPowerSeries σ R
⊢ ℕ∞

Tactic:
exact dite (f = 0) (fun _ => ⊤) fun h =>
    Nat.find ((ne_zero_iff_exists_coeff_ne_zero_and_weight w).mp h)

Premises used: dite, Nat.find, Iff.mp, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, Top.top, OfNat.ofNat, Eq
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f_1 g f : MvPowerSeries σ R
⊢ ℕ∞

Tactic:
classical
  exact dite (f = 0) (fun _ => ⊤) fun h =>
    Nat.find ((ne_zero_iff_exists_coeff_ne_zero_and_weight w).mp h)
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
rw :
  Eq (α := ℕ∞)
    (if x : Eq (α := MvPowerSeries σ R) 0 0 then ⊤
    else
      (↑(Nat.find (p := fun (n : ℕ) ↦
            ∃ (d : σ →₀ ℕ),
              Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R) (0 : R) ∧
                (weight w : (a : σ →₀ ℕ) → ℕ) d = n)
            ⋯) :
        ℕ∞))
    ⊤
rw₁ rw₂ : Eq (α := ℕ∞) ⊤ ⊤
⊢ weightedOrder.{u_1, u_2} (R := R) w 0 = ⊤

Tactic:
rw [weightedOrder, dif_pos rfl]

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

Tactic:
simp only [weightedOrder, ne_eq, coe_toNat_eq_self, dite_eq_left_iff,
    ENat.coe_ne_top, imp_false, not_not]

Premises used: Classical.not_not, imp_false, ne_eq, ENat.coe_toNat_eq_self, MvPowerSeries.weightedOrder, ENat.coe_ne_top, dite_eq_left_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
rw : ¬weightedOrder w f = ⊤ ↔ ¬f = 0
rw₁ : weightedOrder w f ≠ ⊤ ↔ ¬f = 0
rw₂ : weightedOrder w f ≠ ⊤ ↔ f ≠ 0
rw₃ : weightedOrder w f ≠ ⊤ ↔ (↑(weightedOrder w f).toNat : ℕ∞) = weightedOrder w f
rw₄ rw₅ : weightedOrder w f ≠ ⊤ ↔ weightedOrder w f ≠ ⊤
⊢ weightedOrder w f = ⊤ ↔ f = 0

Tactic:
rw [← not_iff_not, ← ne_eq, ← ne_eq, ne_zero_iff_weightedOrder_finite w, coe_toNat_eq_self]

Premises used: not_iff_not, MvPowerSeries.ne_zero_iff_weightedOrder_finite, ne_eq, 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
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) ∧
      (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)
          ⋯
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R) ∧
      (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) = weightedOrder w f

Tactic:
simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]

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
h : (↑(weightedOrder w f).toNat : ℕ∞) = 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

Tactic:
generalize_proofs h1
-- 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
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

Tactic:
Nat.find_spec h1

Premises used: Nat.find_spec
-- 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
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

Tactic:
exact Nat.find_spec h1

Premises used: Nat.find_spec