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 : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos : ∀ (hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
Tactic: by_cases! hi : weight w i < f.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
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
pos :
  ∀ (hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have neg : ∀ (hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
Tactic: by_cases! hi : weight w i < f.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
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos : HMul.hMul (α := R) (β := R) (0 : R) ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) = 0
Tactic: rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
-- 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
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f
pos : HMul.hMul (α := R) (β := R) (0 : R) ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
-- 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
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos : ∀ (hj : (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞) < weightedOrder w g),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
Tactic: by_cases! hj : weight w j < 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
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
pos :
  ∀ (hj : (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞) < weightedOrder w g),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have neg : ∀ (hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
Tactic: by_cases! hj : weight w j < 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
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞) < weightedOrder w g
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos : HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R) (0 : R) = 0
Tactic: rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_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
d : σ →₀ ℕ
hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞) < weightedOrder w g
pos : HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R) (0 : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have pos₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (hypothesis)
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
i j : σ →₀ ℕ
hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have hij₁ : i + j = d
Tactic: simp only [Finset.mem_antidiagonal] at hij
Cleared hypotheses: hij
-- 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
hij : i + j = d
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
have neg : False
Tactic: exfalso
-- 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
hij : i + j = d
⊢ False
have neg : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
Tactic: apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
-- 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
hij : i + j = d
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
have neg : (↑((weight w : (a : σ →₀ ℕ) → ℕ) (i + j)) : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
Tactic: rw [← hij, map_add, Nat.cast_add]
-- 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
hij : i + j = d
neg :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) (i + j)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
have neg₁ : (↑(HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) i : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) j : ℕ)) : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
Tactic: rw [← hij, map_add, Nat.cast_add]
-- 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
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)
hj : weightedOrder w g ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
hij : i + j = d
neg :
  (↑((weight w : (a : σ →₀ ℕ) → ℕ) (i + j)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
neg₁ :
  (↑(HAdd.hAdd (α := ℕ) (β := ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) i : ℕ) ((weight w : (a : σ →₀ ℕ) → ℕ) j : ℕ)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
⊢ (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
have neg₂ : HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) (↑((weight w : (a : σ →₀ ℕ) → ℕ) j) : ℕ∞)
Tactic: rw [← hij, map_add, Nat.cast_add]
-- 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: classical
  apply le_weightedOrder
  intro d hd
  rw [coeff_mul, Finset.sum_eq_zero]
  rintro ⟨i, j⟩ hij
  by_cases! hi : weight w i < f.weightedOrder w
  · rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
  · by_cases! hj : weight w j < g.weightedOrder w
    · rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]
    · simp only [Finset.mem_antidiagonal] at hij
      exfalso
      apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
      rw [← hij, map_add, Nat.cast_add]
-- 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 h₁ :
  ∀ (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)
⊢ weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)
have h₂ : ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g),
  ∀ 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: classical
  apply le_weightedOrder
  intro d hd
  rw [coeff_mul, Finset.sum_eq_zero]
  rintro ⟨i, j⟩ hij
  by_cases! hi : weight w i < f.weightedOrder w
  · rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
  · by_cases! hj : weight w j < g.weightedOrder w
    · rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]
    · simp only [Finset.mem_antidiagonal] at hij
      exfalso
      apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
      rw [← hij, map_add, Nat.cast_add]
-- 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 h₁ :
  ∀ (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)
h₂ :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g),
    ∀ 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
⊢ weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)
have h₃ : ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g) (i j : σ →₀ ℕ)
  (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
Tactic: classical
  apply le_weightedOrder
  intro d hd
  rw [coeff_mul, Finset.sum_eq_zero]
  rintro ⟨i, j⟩ hij
  by_cases! hi : weight w i < f.weightedOrder w
  · rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
  · by_cases! hj : weight w j < g.weightedOrder w
    · rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]
    · simp only [Finset.mem_antidiagonal] at hij
      exfalso
      apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
      rw [← hij, map_add, Nat.cast_add]
-- 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 h₁ :
  ∀ (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)
h₂ :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g),
    ∀ 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
h₃ :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g) (i j : σ →₀ ℕ)
    (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
⊢ weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)
have pos : ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g) (i j : σ →₀ ℕ)
  (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d)
  (hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
Tactic: classical
  apply le_weightedOrder
  intro d hd
  rw [coeff_mul, Finset.sum_eq_zero]
  rintro ⟨i, j⟩ hij
  by_cases! hi : weight w i < f.weightedOrder w
  · rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
  · by_cases! hj : weight w j < g.weightedOrder w
    · rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]
    · simp only [Finset.mem_antidiagonal] at hij
      exfalso
      apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
      rw [← hij, map_add, Nat.cast_add]
-- 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 h₁ :
  ∀ (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)
h₂ :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g),
    ∀ 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
h₃ :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g) (i j : σ →₀ ℕ)
    (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
pos :
  ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g) (i j : σ →₀ ℕ)
    (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d)
    (hi : (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞) < weightedOrder w f),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
      0
⊢ weightedOrder w f + weightedOrder w g ≤ weightedOrder w (f * g)
have neg : ∀ (d : σ →₀ ℕ) (hd : (↑((weight w : (a : σ →₀ ℕ) → ℕ) d) : ℕ∞) < weightedOrder w f + weightedOrder w g) (i j : σ →₀ ℕ)
  (hij : (i, j) ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ d)
  (hi : weightedOrder w f ≤ (↑((weight w : (a : σ →₀ ℕ) → ℕ) i) : ℕ∞)),
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) f : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) g : R) =
    0
Tactic: classical
  apply le_weightedOrder
  intro d hd
  rw [coeff_mul, Finset.sum_eq_zero]
  rintro ⟨i, j⟩ hij
  by_cases! hi : weight w i < f.weightedOrder w
  · rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
  · by_cases! hj : weight w j < g.weightedOrder w
    · rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]
    · simp only [Finset.mem_antidiagonal] at hij
      exfalso
      apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
      rw [← hij, map_add, Nat.cast_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)
⊢ (n + 1) • weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
have succ : n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
Tactic: grw [succ_nsmul, pow_succ, hn, le_weightedOrder_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)
succ : n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
⊢ (n + 1) • weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
have succ₁ : n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ n * f)
Tactic: grw [succ_nsmul, pow_succ, hn, le_weightedOrder_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)
succ : n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
succ₁ : n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ n * f)
⊢ (n + 1) • weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
have succ₂ : weightedOrder w (f ^ n) + weightedOrder w f ≤ weightedOrder w (f ^ n * f)
Tactic: grw [succ_nsmul, pow_succ, hn, le_weightedOrder_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)
succ : n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
succ₁ : n • weightedOrder w f + weightedOrder w f ≤ weightedOrder w (f ^ n * f)
succ₂ : weightedOrder w (f ^ n) + weightedOrder w f ≤ weightedOrder w (f ^ n * f)
⊢ (n + 1) • weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
have succ₃ : weightedOrder w (f ^ n * f) ≤ weightedOrder w (f ^ n * f)
Tactic: grw [succ_nsmul, pow_succ, hn, le_weightedOrder_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ n • weightedOrder w f ≤ weightedOrder w (f ^ n)
have zero : HSMul.hSMul (α := ℕ) 0 (weightedOrder w f) ≤ weightedOrder w (HPow.hPow (β := ℕ) f 0)
Tactic: induction n with
  | zero => simp
  | succ n hn => grw [succ_nsmul, pow_succ, hn, le_weightedOrder_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
zero : HSMul.hSMul (α := ℕ) 0 (weightedOrder w f) ≤ weightedOrder w (HPow.hPow (β := ℕ) f 0)
⊢ n • weightedOrder w f ≤ weightedOrder w (f ^ n)
have succ : ∀ (n : ℕ) (hn : n • weightedOrder w f ≤ weightedOrder w (f ^ n)),
  (n + 1) • weightedOrder w f ≤ weightedOrder w (f ^ (n + 1))
Tactic: induction n with
  | zero => simp
  | succ n hn => grw [succ_nsmul, pow_succ, hn, le_weightedOrder_mul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i)
⊢ ∑ i ∈ Finset.cons a s ha, weightedOrder w (f i) ≤ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ Finset.cons a s ha, f i)
have cons : 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)
Tactic: grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]