awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
hf :
  ∃ (a : ℕ),
    ∀ b ≥ a,
      HPow.hPow (α := R ⧸ I)
          ((constantCoeff : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
              ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) f) :
            R ⧸ I)
          b =
        0
obtain :
  ∀ (N : ℕ)
    (hN :
      ∀ b ≥ N,
        HPow.hPow (α := R ⧸ I)
            ((constantCoeff : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
                ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) f) :
              R ⧸ I)
            b =
          0),
    ∃ (a : ℕ),
      ∀ b ≥ a,
        Eq.{u_3 + 1} (α := R ⧸ I)
          ((coeff d : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
              ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) (f ^ b)) :
            R ⧸ I)
          (0 : R ⧸ I)
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      Eq.{u_3 + 1} (α := R ⧸ I)
        ((coeff d : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
            ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) (f ^ b)) :
          R ⧸ I)
        (0 : R ⧸ I)

Tactic:
obtain ⟨N, hN⟩ := hf
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
N : ℕ
hN :
  ∀ b ≥ N,
    HPow.hPow (α := R ⧸ I)
        ((constantCoeff : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
            ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) f) :
          R ⧸ I)
        b =
      0
h :
  ∀ b ≥ HAdd.hAdd (β := ℕ) N ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ),
    Eq.{u_3 + 1} (α := R ⧸ I)
      ((coeff d : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
          ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) (f ^ b)) :
        R ⧸ I)
      (0 : R ⧸ I)
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      Eq.{u_3 + 1} (α := R ⧸ I)
        ((coeff d : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
            ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) (f ^ b)) :
          R ⧸ I)
        (0 : R ⧸ I)

Tactic:
use N + d.degree

Premises used: Finsupp.degree, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
d : σ →₀ ℕ
I : Ideal R
hI : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
N : ℕ
hN :
  ∀ b ≥ N,
    HPow.hPow (α := R ⧸ I)
        ((constantCoeff : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
            ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) f) :
          R ⧸ I)
        b =
      0
n : ℕ
hn : n ≥ HAdd.hAdd (β := ℕ) N ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) d : ℕ)
⊢ Eq.{u_3 + 1} (α := R ⧸ I)
    ((coeff d : (a : MvPowerSeries σ (R ⧸ I)) → R ⧸ I)
        ((map (Ideal.Quotient.mk I) : (a : MvPowerSeries σ R) → MvPowerSeries σ (R ⧸ I)) (f ^ n)) :
      R ⧸ I)
    (0 : R ⧸ I)

Tactic:
simpa only [map_pow] using coeff_eq_zero_of_constantCoeff_nilpotent (hN N le_rfl) hn

Premises used: le_rfl, MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent, map_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
⊢ Tendsto (β := MvPowerSeries σ R) (fun (n : ℕ) ↦ f ^ n) atTop (𝓝 0) ↔
    IsTopologicallyNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
⟨fun H ↦ ?_, isTopologicallyNilpotent_of_constantCoeff⟩

Premises used: MvPowerSeries.LinearTopology.isTopologicallyNilpotent_of_constantCoeff, Iff.intro
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
refine :
  ∀ (H : Tendsto (β := MvPowerSeries σ R) (fun (n : ℕ) ↦ f ^ n) atTop (𝓝 0)),
    IsTopologicallyNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ Tendsto (β := MvPowerSeries σ R) (fun (n : ℕ) ↦ f ^ n) atTop (𝓝 0) ↔
    IsTopologicallyNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
refine ⟨fun H ↦ ?_, isTopologicallyNilpotent_of_constantCoeff⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
H : Tendsto (β := MvPowerSeries σ R) (fun (n : ℕ) ↦ f ^ n) atTop (𝓝 0)
⊢ Tendsto.{0, u_3} (β := R) (fun (n : ℕ) ↦ (constantCoeff : (a : MvPowerSeries σ R) → R) (f ^ n)) atTop (𝓝 0)

Tactic:
replace H : Tendsto (fun n ↦ constantCoeff (f ^ n)) atTop (nhds 0) :=
    continuous_constantCoeff R |>.tendsto' 0 0 constantCoeff_zero |>.comp H
-- Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsLinearTopology R R
f : MvPowerSeries σ R
H : Tendsto.{0, u_3} (β := R) (fun (n : ℕ) ↦ (constantCoeff : (a : MvPowerSeries σ R) → R) (f ^ n)) atTop (𝓝 0)
⊢ IsTopologicallyNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
simpa only [map_pow] using H

Premises used: map_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
x : MvPowerSeries σ R
hx : x * φ = 0
h :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ x = 0

Tactic:
ext d
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
x : MvPowerSeries σ R
hx : x * φ = 0
d : σ →₀ ℕ
h :
  ∀ (x_1 : σ →₀ ℕ),
    (∀ y < x_1,
        Eq.{u_2 + 1} (α := R) ((coeff y : (a : MvPowerSeries σ R) → R) x : R)
          ((coeff y : (a : MvPowerSeries σ R) → R) 0 : R)) →
      Eq.{u_2 + 1} (α := R) ((coeff x_1 : (a : MvPowerSeries σ R) → R) x : R)
        ((coeff x_1 : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
apply WellFoundedLT.induction d

Premises used: WellFoundedLT.induction
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight 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)
h :
  HMul.hMul (α := R) (β := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) =
    (coeff e : (a : MvPowerSeries σ R) → R) (x * φ)
⊢ Eq.{u_2 + 1} (α := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R) ((coeff e : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]

Premises used: map_zero, mul_right_mem_nonZeroDivisorsRight_eq_zero_iff, MvPowerSeries.coeff
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight 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)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) x : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R) :
      R)
    ((coeff e : (a : MvPowerSeries σ R) → R) (x * φ) : R)

Tactic:
(coeff_mul e x φ).symm

Premises used: Eq.symm, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight 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)
h :
  HMul.hMul (α := R) (β := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) =
    ∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) x : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R)
⊢ HMul.hMul (α := R) (β := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) =
    (coeff e : (a : MvPowerSeries σ R) → R) (x * φ)

Tactic:
convert! (coeff_mul e x φ).symm

Premises used: Eq.symm, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight 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)
h :
  ∀ b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
    b ≠ (e, 0) →
      HMul.hMul (α := R) (β := R) ((coeff b.1 : (a : MvPowerSeries σ R) → R) x : R)
          ((coeff b.2 : (a : MvPowerSeries σ R) → R) φ : R) =
        0
h₁ :
  (e, 0) ∉ @antidiagonal _ Finsupp.instAddMonoid _ e →
    HMul.hMul (α := R) (β := R) ((coeff (e, 0).1 : (a : MvPowerSeries σ R) → R) x : R)
        ((coeff (e, 0).2 : (a : MvPowerSeries σ R) → R) φ : R) =
      0
⊢ HMul.hMul (α := R) (β := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) =
    ∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) x : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff, Prod.mk, Finset.sum_eq_single, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight 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)
u snd : σ →₀ ℕ
huv : (u, snd) ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
h : (u, snd) ≠ (e, 0)
this : u < e
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, snd).1 : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff (u, snd).2 : (a : MvPowerSeries σ R) → R) φ : R) =
    0

Tactic:
simp only [he u this, zero_mul, map_zero]

Premises used: MulZeroClass.zero_mul, map_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight 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)
u snd : σ →₀ ℕ
huv : (u, snd) ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
h_1 : (u, snd) ≠ (e, 0)
h : u < e
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, snd).1 : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff (u, snd).2 : (a : MvPowerSeries σ R) → R) φ : R) =
    0

Tactic:
suffices u < e by simp only [he u this, zero_mul, map_zero]
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight 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)
u snd : σ →₀ ℕ
huv : (u, snd) ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
h_1 : (u, snd) ≠ (e, 0)
h : u ≤ e
h₁ : u ≠ e
⊢ u < e

Tactic:
apply lt_of_le_of_ne

Premises used: lt_of_le_of_ne
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight 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)
u snd : σ →₀ ℕ
huv : (u, snd) ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
h : (u, snd) ≠ (e, 0)
⊢ u ≤ e

Tactic:
simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]

Premises used: zero_le, le_add_iff_nonneg_right, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp
-- Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ : MvPowerSeries σ R
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisorsRight R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
x : MvPowerSeries σ R
hx : x * φ = 0
d u snd : σ →₀ ℕ
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 : (u, snd) ∈ @antidiagonal _ Finsupp.instAddMonoid _ u
h : (u, snd) ≠ (u, 0)
⊢ 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) (nonZeroDivisorsRight 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)
⊢ (e, 0) ∉ @antidiagonal _ Finsupp.instAddMonoid _ e →
    HMul.hMul (α := R) (β := R) ((coeff (e, 0).1 : (a : MvPowerSeries σ R) → R) x : R)
        ((coeff (e, 0).2 : (a : MvPowerSeries σ R) → R) φ : R) =
      0

Tactic:
simp
-- 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
h :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ x = 0

Tactic:
ext d
-- 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 : σ →₀ ℕ
h :
  ∀ (x_1 : σ →₀ ℕ),
    (∀ y < x_1,
        Eq.{u_2 + 1} (α := R) ((coeff y : (a : MvPowerSeries σ R) → R) x : R)
          ((coeff y : (a : MvPowerSeries σ R) → R) 0 : R)) →
      Eq.{u_2 + 1} (α := R) ((coeff x_1 : (a : MvPowerSeries σ R) → R) x : R)
        ((coeff x_1 : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
apply WellFoundedLT.induction d

Premises used: WellFoundedLT.induction
-- 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)
h :
  HMul.hMul (α := R) (β := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) x : R) =
    (coeff e : (a : MvPowerSeries σ R) → R) (φ * x)
⊢ Eq.{u_2 + 1} (α := R) ((coeff e : (a : MvPowerSeries σ R) → R) x : R) ((coeff e : (a : MvPowerSeries σ R) → R) 0 : R)

Tactic:
rw [map_zero, ← mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]

Premises used: map_zero, mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff, MvPowerSeries.coeff
-- 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)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
        HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff p.2 : (a : MvPowerSeries σ R) → R) x : R) :
      R)
    ((coeff e : (a : MvPowerSeries σ R) → R) (φ * x) : R)

Tactic:
(coeff_mul e φ x).symm

Premises used: Eq.symm, MvPowerSeries.coeff_mul
-- 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)
h :
  HMul.hMul (α := R) (β := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) x : R) =
    ∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) x : R)
⊢ HMul.hMul (α := R) (β := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) x : R) =
    (coeff e : (a : MvPowerSeries σ R) → R) (φ * x)

Tactic:
convert! (coeff_mul e φ x).symm

Premises used: Eq.symm, MvPowerSeries.coeff_mul
-- 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)
h :
  ∀ b ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
    b ≠ (0, e) →
      HMul.hMul (α := R) (β := R) ((coeff b.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff b.2 : (a : MvPowerSeries σ R) → R) x : R) =
        0
h₁ :
  (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
⊢ HMul.hMul (α := R) (β := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) x : R) =
    ∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ e,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) x : R)

Tactic:
rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff, Prod.mk, Finset.sum_eq_single, OfNat.ofNat
-- 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)
fst u : σ →₀ ℕ
huv : (fst, u) ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
h : (fst, u) ≠ (0, e)
this : u < e
⊢ HMul.hMul (α := R) (β := R) ((coeff (fst, u).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (fst, u).2 : (a : MvPowerSeries σ R) → R) x : R) =
    0

Tactic:
simp only [he u this, mul_zero, map_zero]

Premises used: map_zero, MulZeroClass.mul_zero
-- 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)
fst u : σ →₀ ℕ
huv : (fst, u) ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
h_1 : (fst, u) ≠ (0, e)
h : u < e
⊢ HMul.hMul (α := R) (β := R) ((coeff (fst, u).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (fst, u).2 : (a : MvPowerSeries σ R) → R) x : R) =
    0

Tactic:
suffices u < e by simp only [he u this, mul_zero, map_zero]
-- 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)
fst u : σ →₀ ℕ
huv : (fst, u) ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
h_1 : (fst, u) ≠ (0, e)
h : u ≤ e
h₁ : u ≠ e
⊢ u < e

Tactic:
apply lt_of_le_of_ne

Premises used: lt_of_le_of_ne
-- 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)
fst u : σ →₀ ℕ
huv : (fst, u) ∈ @antidiagonal _ Finsupp.instAddMonoid _ e
h : (fst, u) ≠ (0, e)
⊢ u ≤ e

Tactic:
simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]

Premises used: zero_le, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp, le_add_iff_nonneg_left