awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) = ⊤
have pos₂ : Eq (α := MvPowerSeries σ R) 0 0
Tactic: rw [h, weightedOrder_eq_top_iff, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have 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)
Tactic: rw [weightedOrder_eq_nat]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
⊢ (∃ (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)
have 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 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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 : σ →₀ ℕ),
      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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
h : ¬a = 0
⊢ ∃ (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 : ℕ)
have 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 : ℕ)
Tactic: use d
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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 : ℕ)
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff b : (a : MvPowerSeries σ R) → R) ((monomial d : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) : R)
    (0 : R)
have neg : ¬b = d
Tactic: rw [coeff_monomial, if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst_1 : Decidable (a = 0)
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have pos : ∀ (h : a = 0), weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) = ⊤
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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) = ⊤
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    if a = 0 then ⊤ else (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have neg : ∀ (h : ¬a = 0),
  weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((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
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have rw : Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: rw [weightedOrder_monomial, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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) : ℕ∞)
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: rw [weightedOrder_monomial, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have rw : Eq (α := ℕ∞) (if a = 0 then ⊤ else (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: classical
  rw [weightedOrder_monomial, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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) : ℕ∞)
⊢ weightedOrder.{u_1, u_2} (R := R) w ((monomial d : (a : R) → MvPowerSeries σ R) a) =
    (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞)
Tactic: classical
  rw [weightedOrder_monomial, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ min (weightedOrder w f) (weightedOrder w g) ≤ weightedOrder w (f + g)
have 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)
Tactic: apply le_weightedOrder w
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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) = weightedOrder w f
have obtain : ∀ (n : ℕ) (hn : (↑n : ℕ∞) = 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)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ weightedOrder w (f + g) = weightedOrder w f
have 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)
Tactic: rw [← hn, weightedOrder_eq_nat]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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 : σ →₀ ℕ),
      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)
have 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)
Tactic: obtain ⟨d, hd', hd⟩ := ((weightedOrder_eq_nat w).mp hn.symm).1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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) ∧
    ∀ (d : σ →₀ ℕ),
      (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
        Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have left : ∃ (d : σ →₀ ℕ),
  Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R) ∧
    (weight w : (a : σ →₀ ℕ) → ℕ) d = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ (∃ (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)
have right : ∀ (d : σ →₀ ℕ),
  (weight w : (a : σ →₀ ℕ) → ℕ) d < n →
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
have left : Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
Tactic: refine ⟨d, ?_, hd⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ Ne.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have 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)
Tactic: rw [← hn, ← hd] at H
Cleared hypotheses: H, hn, d, hd', hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have rw : HAdd.hAdd (α := R) (β := R) ((coeff b : (a : MvPowerSeries σ R) → R) f : R)
    ((coeff b : (a : MvPowerSeries σ R) → R) g : R) =
  0
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have rw₁ : HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff b : (a : MvPowerSeries σ R) → R) g : R) = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have rw₂ : HAdd.hAdd (α := R) 0 0 = 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have rw₃ : Eq.{u_2 + 1} (α := R) 0 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff b : (a : MvPowerSeries σ R) → R) (f + g) : R) (0 : R)
have right : (↑((weight w : (a : σ →₀ ℕ) → ℕ) b) : ℕ∞) < weightedOrder w f
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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)
have refine : weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
Tactic: refine le_antisymm ?_ (min_weightedOrder_le_add w)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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)
have 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)
Tactic: wlog H₁ : f.weightedOrder w < g.weightedOrder w
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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)
⊢ weightedOrder w (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
have 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)
Tactic: wlog H₁ : f.weightedOrder w < g.weightedOrder w
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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 (f + g) ≤ min (weightedOrder w f) (weightedOrder w g)
have inr : weightedOrder w (g + f) ≤ min (weightedOrder w g) (weightedOrder w f)
Tactic: rw [add_comm f g, inf_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
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 + g) ≤ min (weightedOrder w f) (weightedOrder w g)
have simp : weightedOrder w f ≤ weightedOrder w f ∧ weightedOrder w f ≤ weightedOrder w g
Tactic: simp only [le_inf_iff, weightedOrder_add_of_weightedOrder_lt.aux w H₁]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)
have h : ∀ (d : σ →₀ ℕ),
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g →
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
Tactic: apply le_weightedOrder
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f * g) : R) (0 : R)
have h : ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d,
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
Tactic: rw [coeff_mul, Finset.sum_eq_zero]