awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsLeft R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
x : MvPowerSeries σ R
hx : φ * x = 0
d fst u : σ →₀ ℕ
he :
  ∀ y < u,
    Eq.{u_2 + 1} (α := R) ((coeff y : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff y : (a : MvPowerSeries σ R) → R) 0 : R)
huv : (fst, u) ∈ @antidiagonal _ Finsupp.instAddMonoid _ u
h : (fst, u) ≠ (0, u)
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsLeft R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
x : MvPowerSeries σ R
hx : φ * x = 0
d e : σ →₀ ℕ
he :
  ∀ y < e,
    Eq.{u_2 + 1} (α := R) ((coeff y : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff y : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ (0, e) ∉ @antidiagonal _ Finsupp.instAddMonoid _ e →
    HMul.hMul (α := R) (β := R) ((coeff (0, e).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (0, e).2 : (a : MvPowerSeries σ R) → R) x : R) =
      0

Tactic:
simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff, not_true_eq_false, zero_add, false_implies, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ : Membership.mem (α := R) (γ := Submonoid R) R⁰ ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (MvPowerSeries σ R)⁰ φ

Tactic:
⟨mem_nonZeroDivisorsLeft_of_constantCoeff hφ.1, mem_nonZeroDivisorsRight_of_constantCoeff hφ.2⟩

Premises used: Set.Mem, setOf, Set.inter, MvPowerSeries.mem_nonZeroDivisorsLeft_of_constantCoeff, And.right, And.left, And.intro, MvPowerSeries.mem_nonZeroDivisorsRight_of_constantCoeff
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
mp :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
      ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) →
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) r
mpr :
  Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) r →
    Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R))
      (nonZeroDivisorsLeft (MvPowerSeries σ R)) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
⊢ Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
      ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) ↔
    Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) r

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
    ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : r * s = 0
rw :
  Eq (α := MvPowerSeries σ R) ((monomial (n + 0) : (a : R) → MvPowerSeries σ R) (r * s) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
⊢ HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      ((C : (a : R) → MvPowerSeries σ R) s : MvPowerSeries σ R) =
    0

Tactic:
rw [← monomial_zero_eq_C, monomial_mul_monomial]

Premises used: MvPowerSeries.monomial_zero_eq_C, MvPowerSeries.monomial_mul_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
    ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : r * s = 0
h :
  ∀ (n_1 : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R)
          ((monomial (n + 0) : (a : R) → MvPowerSeries σ R) (r * s) : MvPowerSeries σ R) :
        R)
      ((coeff n_1 : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Eq (α := MvPowerSeries σ R) ((monomial (n + 0) : (a : R) → MvPowerSeries σ R) (r * s) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
    ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : r * s = 0
n_1 : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff n_1 : (a : MvPowerSeries σ R) → R)
        ((monomial (n + 0) : (a : R) → MvPowerSeries σ R) (r * s) : MvPowerSeries σ R) :
      R)
    ((coeff n_1 : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
simp [hrs]
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
    ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : r * s = 0
⊢ 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])
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H :
  Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
    ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : r * s = 0
this : Eq (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) s : MvPowerSeries σ R) (0 : MvPowerSeries σ R)
⊢ s = 0

Tactic:
simpa using congr(coeff 0 $(this))
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) r
p : MvPowerSeries σ R
hrp : HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) p = 0
mpr :
  ∀ (i : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R)
      ((coeff i : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ p = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) r
p : MvPowerSeries σ R
hrp : HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) p = 0
i : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff (i + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) p) :
      R)
    ((coeff (i + n) : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
have := congr(coeff (i + n) $hrp)
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) r
p : MvPowerSeries σ R
hrp : HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) p = 0
i : σ →₀ ℕ
this :
  Eq.{u_2 + 1} (α := R)
    ((coeff (i + n) : (a : MvPowerSeries σ R) → R)
        (HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) p) :
      R)
    ((coeff (i + n) : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ HMul.hMul (β := R) r ((coeff i : (a : MvPowerSeries σ R) → R) p : R) = (coeff (i + n) : (a : MvPowerSeries σ R) → R) 0

Tactic:
rw [coeff_monomial_mul, if_pos le_add_self, add_tsub_cancel_right] at this

Premises used: MvPowerSeries.coeff_monomial_mul, if_pos, add_tsub_cancel_right, le_add_self
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
H : Membership.mem (γ := Submonoid R) (nonZeroDivisorsLeft R) r
p : MvPowerSeries σ R
hrp : HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) p = 0
i : σ →₀ ℕ
this :
  HMul.hMul (β := R) r ((coeff i : (a : MvPowerSeries σ R) → R) p : R) = (coeff (i + n) : (a : MvPowerSeries σ R) → R) 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R) ((coeff i : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
simpa using H _ this
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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
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)
⊢ 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

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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
rw :
  Eq (α := MvPowerSeries σ R) ((monomial (0 + n) : (a : R) → MvPowerSeries σ R) (s * r) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
⊢ HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) s : MvPowerSeries σ R)
      ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) =
    0

Tactic:
rw [← monomial_zero_eq_C, monomial_mul_monomial]

Premises used: MvPowerSeries.monomial_zero_eq_C, MvPowerSeries.monomial_mul_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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
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)
⊢ Eq (α := MvPowerSeries σ R) ((monomial (0 + n) : (a : R) → MvPowerSeries σ R) (s * r) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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
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:
simp [hrs]
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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) ((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])
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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
this : Eq (α := MvPowerSeries σ R) ((C : (a : R) → MvPowerSeries σ R) s : MvPowerSeries σ R) (0 : MvPowerSeries σ R)
⊢ s = 0

Tactic:
simpa using congr(coeff 0 $(this))
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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
mpr :
  ∀ (i : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R)
      ((coeff i : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ p = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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 + 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)
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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)
⊢ 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

Premises used: MvPowerSeries.coeff_mul_monomial, if_pos, add_tsub_cancel_right, le_add_self
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
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 :
  HMul.hMul (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R) r = (coeff (i + n) : (a : MvPowerSeries σ R) → R) 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff i : (a : MvPowerSeries σ R) → R) p : R) ((coeff i : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
simpa using H _ this
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : R
⊢ Membership.mem (α := MvPowerSeries σ R) (γ := Submonoid (MvPowerSeries σ R)) (MvPowerSeries σ R)⁰
      ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) ↔
    Membership.mem (γ := Submonoid R) R⁰ r

Tactic:
monomial_mem_nonzeroDivisorsLeft.and monomial_mem_nonzeroDivisorsRight

Premises used: MvPowerSeries.monomial_mem_nonzeroDivisorsLeft, Set.Mem, setOf, MvPowerSeries.monomial_mem_nonzeroDivisorsRight, Set.inter, Iff.and
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
i : σ
rw : Membership.mem (γ := Submonoid R) R⁰ 1
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (MvPowerSeries σ R)⁰ (X i)

Tactic:
rw [X, monomial_mem_nonzeroDivisors]

Premises used: MvPowerSeries.monomial_mem_nonzeroDivisors, MvPowerSeries.X
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
i : σ
⊢ Membership.mem (γ := Submonoid R) R⁰ 1

Tactic:
Submonoid.one_mem R⁰

Premises used: Set.Mem, nonZeroDivisors, Submonoid.one_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
i : σ
⊢ Membership.mem (γ := Submonoid R) R⁰ 1

Tactic:
exact Submonoid.one_mem R⁰

Premises used: nonZeroDivisors, Submonoid.one_mem
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
h : φ * ψ = 0
rcases : ∀ (w : LinearOrder σ), WellFoundedGT σ → φ = 0 ∨ ψ = 0
⊢ φ = 0 ∨ ψ = 0

Tactic:
rcases exists_wellFoundedGT σ

Premises used: exists_wellFoundedGT
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
h : φ * ψ = 0
w : LinearOrder σ
h_1 : WellFoundedGT σ
⊢ φ = 0 ∨ ψ = 0

Tactic:
simpa only [← lexOrder_eq_top_iff_eq_zero, lexOrder_mul, WithTop.add_eq_top] using h

Premises used: MvPowerSeries.lexOrder_mul, WithTop.add_eq_top, MvPowerSeries.lexOrder_eq_top_iff_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
apply : weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
⊢ weightedOrder w (f * g) = weightedOrder w f + weightedOrder w g

Tactic:
apply le_antisymm _ (le_weightedOrder_mul w)

Premises used: MvPowerSeries.le_weightedOrder_mul, le_antisymm
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
pos : ∀ (hf : weightedOrder w f < ⊤), weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
neg : ∀ (hf : ¬weightedOrder w f < ⊤), weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

Tactic:
by_cases hf : f.weightedOrder w < ⊤

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

Tactic:
by_cases hg : g.weightedOrder w < ⊤

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

Tactic:
simpa only [p, ENat.coe_toNat_eq_self, ← lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top, ENat.coe_toNat_eq_self
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
⊢ (↑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]
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
⊢ (↑q : ℕ∞) = weightedOrder w g

Tactic:
simpa only [q, ENat.coe_toNat_eq_self, ← lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top, ENat.coe_toNat_eq_self
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
⊢ (↑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]
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : (↑p : ℕ∞) = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : (↑q : ℕ∞) = weightedOrder w g
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))
⊢ 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:
simp only [ne_eq, mul_eq_zero]

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

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

Tactic:
weightedHomogeneousComponent_of_weightedOrder ?_ H

Premises used: MvPowerSeries.weightedHomogeneousComponent_of_weightedOrder