awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg :
  (∃ (d_1 : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R)
          ((coeff d_1 : (a : MvPowerSeries σ R) → R)
              ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          (0 : R) ∧
        Eq (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d_1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ)) ∧
    ∀ (d_1 : σ →₀ ℕ),
      LT.lt (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d_1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ) →
        Eq.{u_2 + 1} (α := R)
          ((coeff d_1 : (a : MvPowerSeries σ R) → R)
              ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          (0 : R)
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
rw [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
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
neg :
  ∃ (d_1 : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R)
        ((coeff d_1 : (a : MvPowerSeries σ R) → R) ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
          R)
        (0 : R) ∧
      Eq (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d_1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ)
neg₁ :
  ∀ (d_1 : σ →₀ ℕ),
    LT.lt (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d_1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ) →
      Eq.{u_2 + 1} (α := R)
        ((coeff d_1 : (a : MvPowerSeries σ R) → R) ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
          R)
        (0 : R)
⊢ (∃ (d_1 : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R)
          ((coeff d_1 : (a : MvPowerSeries σ R) → R)
              ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          (0 : R) ∧
        Eq (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d_1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ)) ∧
    ∀ (d_1 : σ →₀ ℕ),
      LT.lt (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d_1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ) →
        Eq.{u_2 + 1} (α := R)
          ((coeff d_1 : (a : MvPowerSeries σ R) → R)
              ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
            R)
          (0 : R)

Tactic:
constructor
-- 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
h₁ :
  Ne.{u_2 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R) ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) : R)
      (0 : R) ∧
    Eq (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ)
⊢ ∃ (d_1 : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R)
        ((coeff d_1 : (a : MvPowerSeries σ R) → R) ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) :
          R)
        (0 : R) ∧
      Eq (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d_1 : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ)

Tactic:
use d
-- 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
⊢ Ne.{u_2 + 1} (α := R)
      ((coeff d : (a : MvPowerSeries σ R) → R) ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) : R)
      (0 : R) ∧
    Eq (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ)

Tactic:
simp only [coeff_monomial_same, ne_eq, h, not_false_eq_true, and_self]

Premises used: and_self, MvPowerSeries.coeff_monomial_same, ne_eq, not_false_eq_true
-- 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
b : σ →₀ ℕ
hb : LT.lt (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) b : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) d : ℕ)
neg : ¬b = d
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff b : (a : MvPowerSeries σ R) → R) ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) : R)
    (0 : R)

Tactic:
rw [coeff_monomial, if_neg]

Premises used: MvPowerSeries.coeff_monomial, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : LT.lt (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) b : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) b : ℕ)
⊢ False

Tactic:
hb.false

Premises used: LT.lt.false
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : LT.lt (α := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) b : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) b : ℕ)
⊢ False

Tactic:
exact hb.false

Premises used: LT.lt.false
-- 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 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:
classical
  split_ifs with h
  · rw [h, weightedOrder_eq_top_iff, map_zero]
  · rw [weightedOrder_eq_nat]
    constructor
    · use d
      simp only [coeff_monomial_same, ne_eq, h, not_false_eq_true, and_self]
    · intro b hb
      rw [coeff_monomial, if_neg]
      rintro rfl
      exact hb.false

Premises used: and_self, MvPowerSeries.coeff_monomial_same, map_zero, ne_eq, MvPowerSeries.weightedOrder_eq_nat, MvPowerSeries.coeff_monomial, not_false_eq_true, MvPowerSeries.weightedOrder_eq_top_iff, if_neg, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
h : a ≠ 0
rw :
  Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞))
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
rw [weightedOrder_monomial, if_neg h]

Premises used: MvPowerSeries.weightedOrder_monomial, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
h : a ≠ 0
rw :
  Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞))
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)

Tactic:
classical
  rw [weightedOrder_monomial, if_neg h]

Premises used: MvPowerSeries.weightedOrder_monomial, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
inst_1 : Nontrivial R
⊢ weightedOrder.{u_1, u_2} (R := R) w 1 = 0

Tactic:
weightedOrder_monomial_of_ne_zero w one_ne_zero

Premises used: Multiset.sum, Multiset.foldr, MvPowerSeries.weightedOrder_monomial_of_ne_zero, Finsupp.sum, WithTop.some, one_ne_zero, List.foldr, Finset.sum
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
apply :
  ∀ (d : σ →₀ ℕ),
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < min (weightedOrder w f) (weightedOrder w g) →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
⊢ min (weightedOrder w f) (weightedOrder w g) ≤ weightedOrder w (f + g)

Tactic:
apply le_weightedOrder w

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

Tactic:
simp +contextual only
    [coeff_eq_zero_of_lt_weightedOrder w, lt_min_iff, map_add, add_zero,
      imp_true_iff]

Premises used: map_add, imp_true_iff, add_zero, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder, lt_min_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
obtain : ∀ (n : ℕ) (hn : (↑n : ℕ∞) = weightedOrder w f), weightedOrder w (f + g) = weightedOrder w f
⊢ weightedOrder w (f + g) = weightedOrder w f

Tactic:
obtain ⟨n, hn : (n : ℕ∞) = _⟩ := ENat.ne_top_iff_exists.mp (ne_top_of_lt H)

Premises used: ENat.ne_top_iff_exists, Iff.mp, ne_top_of_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
rw :
  (∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : 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 + g) : R) (0 : R)
⊢ weightedOrder w (f + g) = weightedOrder w f

Tactic:
rw [← hn, 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
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
obtain :
  ∀ (d : σ →₀ ℕ) (hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R))
    (hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n),
    (∃ (d : σ →₀ ℕ),
        Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : 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 + g) : R) (0 : R)
⊢ (∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : 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 + g) : R) (0 : R)

Tactic:
obtain ⟨d, hd', hd⟩ := ((weightedOrder_eq_nat w).mp hn.symm).1

Premises used: MvPowerSeries.weightedOrder_eq_nat, And.left, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
left :
  ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R) ∧
      (weight w : (a : σ →₀ ℕ) → ℕ) d = n
right :
  ∀ (d : σ →₀ ℕ),
    (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
      Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
⊢ (∃ (d : σ →₀ ℕ),
      Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : 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 + g) : R) (0 : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R) ∧
      (weight w : (a : σ →₀ ℕ) → ℕ) d = n

Tactic:
⟨d, ?_, hd⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
left : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
⊢ ∃ (d : σ →₀ ℕ),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R) ∧
      (weight w : (a : σ →₀ ℕ) → ℕ) d = n

Tactic:
refine ⟨d, ?_, hd⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
left :
  ∀ (hn : (↑n : ℕ∞) = weightedOrder w f) (d : σ →₀ ℕ)
    (H : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g)
    (hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R))
    (hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n),
    Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)

Tactic:
rw [← hn, ← hd] at H
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
H : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
left : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)

Tactic:
rw [(coeff _).map_add, coeff_eq_zero_of_lt_weightedOrder w H, add_zero]

Premises used: LinearMap.map_add, MvPowerSeries.coeff, add_zero, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
H : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w g
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)

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

Tactic:
exact hd'
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
b : σ →₀ ℕ
hb : (weight w : (a : σ →₀ ℕ) → ℕ) b < n
this : (↑((weight w : (a : σ →₀ ℕ) → ℕ) b) : ℕ∞) < weightedOrder w f
rw :
  HAdd.hAdd (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff b : (a : MvPowerSeries σ R) → R) g : R) =
    0
rw₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff b : (a : MvPowerSeries σ R) → R) g : R) = 0
rw₂ : HAdd.hAdd (α := R) 0 0 = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)

Tactic:
rw [(coeff _).map_add, coeff_eq_zero_of_lt_weightedOrder w this,
        coeff_eq_zero_of_lt_weightedOrder w (lt_trans this H), add_zero]

Premises used: LinearMap.map_add, lt_trans, MvPowerSeries.coeff, add_zero, MvPowerSeries.coeff_eq_zero_of_lt_weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
b : σ →₀ ℕ
hb : (weight w : (a : σ →₀ ℕ) → ℕ) b < n
right : (↑((weight w : (a : σ →₀ ℕ) → ℕ) b) : ℕ∞) < weightedOrder w f
⊢ Eq.{u_2 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)

Tactic:
suffices weight w b < weightedOrder w f by
      rw [(coeff _).map_add, coeff_eq_zero_of_lt_weightedOrder w this,
        coeff_eq_zero_of_lt_weightedOrder w (lt_trans this H), add_zero]
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
b : σ →₀ ℕ
hb : (weight w : (a : σ →₀ ℕ) → ℕ) b < n
right : (weight w : (a : σ →₀ ℕ) → ℕ) b < n
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) b) : ℕ∞) < weightedOrder w f

Tactic:
rw [← hn, Nat.cast_lt]

Premises used: Nat.cast_lt
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
b : σ →₀ ℕ
hb : (weight w : (a : σ →₀ ℕ) → ℕ) b < n
⊢ (weight w : (a : σ →₀ ℕ) → ℕ) b < n

Tactic:
hb
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : (↑n : ℕ∞) = weightedOrder w f
d : σ →₀ ℕ
hd' : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
hd : (weight w : (a : σ →₀ ℕ) → ℕ) d = n
b : σ →₀ ℕ
hb : (weight w : (a : σ →₀ ℕ) → ℕ) b < n
⊢ (weight w : (a : σ →₀ ℕ) → ℕ) b < n

Tactic:
exact hb
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
⊢ weightedOrder w (f + g) = min (weightedOrder w f) (weightedOrder w g)

Tactic:
le_antisymm ?_ (min_weightedOrder_le_add w)

Premises used: MvPowerSeries.min_weightedOrder_le_add, le_antisymm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
refine : weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
⊢ weightedOrder w (f + g) = min (weightedOrder w f) (weightedOrder w g)

Tactic:
refine le_antisymm ?_ (min_weightedOrder_le_add w)

Premises used: MvPowerSeries.min_weightedOrder_le_add, le_antisymm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
inr :
  ∀
    (this :
      ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R}
        (h : weightedOrder w f ≠ weightedOrder w g) (H₁ : weightedOrder w f < weightedOrder w g),
        weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g))
    (H₁ : ¬weightedOrder w f < weightedOrder w g), weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
wlog :
  ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R}
    (h : weightedOrder w f ≠ weightedOrder w g) (H₁ : weightedOrder w f < weightedOrder w g),
    weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
⊢ weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)

Tactic:
wlog H₁ : f.weightedOrder w < g.weightedOrder w

Premises used: MvPowerSeries.weightedOrder
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
this :
  ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R}
    (h : weightedOrder w f ≠ weightedOrder w g) (H₁ : weightedOrder w f < weightedOrder w g),
    weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
H₁ : ¬weightedOrder w f < weightedOrder w g
inr : weightedOrder w (g + f) ≤ min (weightedOrder w g) (weightedOrder w f)
⊢ weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)

Tactic:
rw [add_comm f g, inf_comm]

Premises used: inf_comm, add_comm
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
this :
  ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R}
    (h : weightedOrder w f ≠ weightedOrder w g) (H₁ : weightedOrder w f < weightedOrder w g),
    weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (g + f) ≤ min (weightedOrder w g) (weightedOrder w f)

Tactic:
this _ h.symm ((le_of_not_gt H₁).lt_of_ne' h)

Premises used: le_of_not_gt, Ne.symm, LE.le.lt_of_ne'
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
this :
  ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R}
    (h : weightedOrder w f ≠ weightedOrder w g) (H₁ : weightedOrder w f < weightedOrder w g),
    weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
H₁ : ¬weightedOrder w f < weightedOrder w g
⊢ weightedOrder w (g + f) ≤ min (weightedOrder w g) (weightedOrder w f)

Tactic:
exact this _ h.symm ((le_of_not_gt H₁).lt_of_ne' h)

Premises used: le_of_not_gt, Ne.symm, LE.le.lt_of_ne'
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ_1 : Type u_1
R_1 : Type u_2
inst : Semiring R_1
w_1 : σ_1 → ℕ
f_1 g_1 : MvPowerSeries σ_1 R_1
σ : Type u_1
R : Type u_2
inst_1 : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
simp : weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g
⊢ weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)

Tactic:
simp only [le_inf_iff, weightedOrder_add_of_weightedOrder_lt.aux w H₁]

Premises used: _private.0.MvPowerSeries.weightedOrder_add_of_weightedOrder_lt.aux, le_inf_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.Order
Goal:
σ_1 : Type u_1
R_1 : Type u_2
inst : Semiring R_1
w_1 : σ_1 → ℕ
f_1 g_1 : MvPowerSeries σ_1 R_1
σ : Type u_1
R : Type u_2
inst_1 : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
h : weightedOrder w f ≠ weightedOrder w g
H₁ : weightedOrder w f < weightedOrder w g
⊢ weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g

Tactic:
⟨le_rfl, le_of_lt H₁⟩

Premises used: le_rfl, le_of_lt, And.intro