awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
mp :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R))
      (nonZeroDivisorsRight (MvPowerSeries σ R)) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) →
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r
⊢ Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R))
      (nonZeroDivisorsRight (MvPowerSeries σ R)) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r
have mpr : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r →
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R))
    (nonZeroDivisorsRight (MvPowerSeries σ R)) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R))
    (nonZeroDivisorsRight (MvPowerSeries σ R)) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : s * r = 0
⊢ HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) s : MvPowerSeries σ R)
      ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) =
    0
have rw : Eq (α := MvPowerSeries σ R) ((monomial (0 + n) : (a : R) → MvPowerSeries σ R) (s * r) : MvPowerSeries σ R)
  (0 : MvPowerSeries σ R)
Tactic: rw [← monomial_zero_eq_C, monomial_mul_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R))
    (nonZeroDivisorsRight (MvPowerSeries σ R)) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : s * r = 0
⊢ Eq (α := MvPowerSeries σ R) ((monomial (0 + n) : (a : R) → MvPowerSeries σ R) (s * r) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
have h : ∀ (n_1 : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R)
    ((coeff n_1 : (a : MvPowerSeries σ R) → R)
        ((monomial (0 + n) : (a : R) → MvPowerSeries σ R) (s * r) : MvPowerSeries σ R) :
      R)
    ((coeff n_1 : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R))
    (nonZeroDivisorsRight (MvPowerSeries σ R)) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : s * r = 0
⊢ s = 0
have this : Eq (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) s : MvPowerSeries σ R) (0 : MvPowerSeries σ R)
Tactic: have := H (C s) (by rw [← monomial_zero_eq_C, monomial_mul_monomial]; ext; simp [hrs])
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r
p : MvPowerSeries σ R
hrp : HMul.hMul (β := MvPowerSeries σ R) p ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) = 0
⊢ p = 0
have mpr : ∀ (i : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R) ((coeff i : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r
p : MvPowerSeries σ R
hrp : HMul.hMul (β := MvPowerSeries σ R) p ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) = 0
i : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R) ((coeff i : (a : MvPowerSeries σ R) → R) 0 : R)
have this : Eq.{u_2 + 1} (α := R)
  ((coeff (i + n) : (a : MvPowerSeries σ R) → R)
      (HMul.hMul (β := MvPowerSeries σ R) p ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)) :
    R)
  ((coeff (i + n) : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: have := congr(coeff (i + n) $hrp)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H : Membership.mem (γ := Submonoid R) (nonZeroDivisorsRight R) r
p : MvPowerSeries σ R
hrp : HMul.hMul (β := MvPowerSeries σ R) p ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) = 0
i : σ →₀ ℕ
this :
  Eq.{u_2 + 1} (α := R)
    ((coeff (i + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (β := MvPowerSeries σ R) p ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)) :
      R)
    ((coeff (i + n) : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R) ((coeff i : (a : MvPowerSeries σ R) → R) 0 : R)
have this₁ : HMul.hMul (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R) r = (coeff (i + n) : (a : MvPowerSeries σ R) → R) 0
Tactic: rw [coeff_mul_monomial, if_pos le_add_self, add_tsub_cancel_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
i : σ
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (MvPowerSeries σ R)⁰ (X i)
have rw : Membership.mem (γ := Submonoid R) R⁰ 1
Tactic: rw [X, monomial_mem_nonzeroDivisors]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
h : φ * ψ = 0
⊢ φ = 0 ∨ ψ = 0
have rcases : ∀ (w : LinearOrder σ), WellFoundedGT σ → φ = 0 ∨ ψ = 0
Tactic: rcases exists_wellFoundedGT σ
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ weightedOrder w (f * g) = weightedOrder w f + weightedOrder w g
have apply : weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
Tactic: apply le_antisymm _ (le_weightedOrder_mul w)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
have pos : ∀ (hf : weightedOrder w f < ⊤), weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
Tactic: by_cases hf : f.weightedOrder w < ⊤
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
pos : ∀ (hf : weightedOrder w f < ⊤), weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
have neg : ∀ (hf : ¬weightedOrder w f < ⊤), weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
Tactic: by_cases hf : f.weightedOrder w < ⊤
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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
have pos : ∀ (hg : weightedOrder w g < ⊤), weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
Tactic: by_cases hg : g.weightedOrder w < ⊤
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
pos : ∀ (hg : weightedOrder w g < ⊤), weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
have neg : ∀ (hg : ¬weightedOrder w g < ⊤), weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
Tactic: by_cases hg : g.weightedOrder w < ⊤
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (hypothesis)
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
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
have hp : (↑p : ℕ∞) = weightedOrder w f
Tactic: have hp : p = f.weightedOrder w := by
        simpa only [p, ENat.coe_toNat_eq_self, ← lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (hypothesis)
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
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
have hq : (↑q : ℕ∞) = weightedOrder w g
Tactic: have hq : q = g.weightedOrder w := by
        simpa only [q, ENat.coe_toNat_eq_self, ← lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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
have simp : ¬(Eq (α := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
      (0 : MvPowerSeries σ R) ∨
    Eq (α := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
      (0 : MvPowerSeries σ R))
Tactic: simp only [ne_eq, mul_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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) ∨
    Eq (α := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
      (0 : MvPowerSeries σ R)
⊢ False
have inl : ∀
  (H :
    Eq (α := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
      (0 : MvPowerSeries σ R)),
  False
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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) ∨
    Eq (α := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
      (0 : MvPowerSeries σ R)
inl :
  ∀
    (H :
      Eq (α := MvPowerSeries σ R)
        ((weightedHomogeneousComponent w p : (a : MvPowerSeries σ R) → MvPowerSeries σ R) f : MvPowerSeries σ R)
        (0 : MvPowerSeries σ R)),
    False
⊢ False
have inr : ∀
  (H :
    Eq (α := MvPowerSeries σ R)
      ((weightedHomogeneousComponent w q : (a : MvPowerSeries σ R) → MvPowerSeries σ R) g : MvPowerSeries σ R)
      (0 : MvPowerSeries σ R)),
  False
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ (↑p : ℕ∞) = weightedOrder w f
have inl : ¬f = 0
Tactic: simp only [ENat.coe_toNat_eq_self, ne_eq, weightedOrder_eq_top_iff, p, q]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ (↑q : ℕ∞) = weightedOrder w g
have inr : ¬g = 0
Tactic: simp only [ENat.coe_toNat_eq_self, ne_eq, weightedOrder_eq_top_iff, p, q]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (hypothesis)
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
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
have 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
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))
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (hypothesis)
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
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
have pos : ¬(↑(p + q) : ℕ∞) < weightedOrder w (f * g)
Tactic: rw [← hp, ← hq, ← Nat.cast_add, ← not_lt]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ False
have pos : Eq (α := MvPowerSeries σ R)
  ((weightedHomogeneousComponent w (p + q) : (a : MvPowerSeries σ R) → MvPowerSeries σ R) (f * g) : MvPowerSeries σ R)
  (0 : MvPowerSeries σ R)
Tactic: apply this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (hypothesis)
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
have hg₁ : weightedOrder w g = ⊤
Tactic: rw [not_lt_top_iff] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (hypothesis)
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
have hf₁ : weightedOrder w f = ⊤
Tactic: rw [not_lt_top_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Finset.sum_cons ha, Finset.prod_cons ha, weightedOrder_mul, ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ 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)
have cons₁ : weightedOrder w (f a * ∏ x ∈ s, f x) = weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x)
Tactic: rw [Finset.sum_cons ha, Finset.prod_cons ha, weightedOrder_mul, ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Finset.sum_cons ha, Finset.prod_cons ha, weightedOrder_mul, ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ 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)
have cons₃ : weightedOrder w (f a) + ∑ i ∈ s, weightedOrder w (f i) = weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x)
Tactic: rw [Finset.sum_cons ha, Finset.prod_cons ha, weightedOrder_mul, ih]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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 ι
⊢ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i) = ∑ i ∈ s, weightedOrder w (f i)
have empty : weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, 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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ weightedOrder.{u_1, u_3} (R := R) w (∏ i ∈ s, f i) = ∑ i ∈ s, weightedOrder w (f i)
have 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)
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]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Order (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
w : σ → ℕ
⊢ weightedOrder.{u_1, u_2} (R := R) w 0 = ⊤
have 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)
          sorry) :
      ℕ∞))
  ⊤
Tactic: rw [weightedOrder, dif_pos rfl]