awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use N + d.degree
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (goal)
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)
have refine : ∀ (H : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.LinearTopology (hypothesis)
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)
⊢ IsTopologicallyNilpotent.{u_3} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
have H₁ : 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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
⊢ x = 0
have h : ∀ (d : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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 : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
have 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)
Tactic: apply WellFoundedLT.induction d
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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) ((coeff e : (a : MvPowerSeries σ R) → R) x : R) ((coeff e : (a : MvPowerSeries σ R) → R) 0 : R)
have 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 * φ)
Tactic: rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ 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 * φ)
have 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)
Tactic: convert! (coeff_mul e x φ).symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ 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)
have 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
Tactic: rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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
⊢ 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)
have 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
Tactic: rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ HMul.hMul (α := R) (β := R) ((coeff (u, snd).1 : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff (u, snd).2 : (a : MvPowerSeries σ R) → R) φ : R) =
    0
have h : u < e
Tactic: suffices u < e by simp only [he u this, zero_mul, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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
have h : u ≤ e
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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
⊢ u < e
have h₁ : u ≠ e
Tactic: apply lt_of_le_of_ne
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsRight (MvPowerSeries σ R)) φ
have intro : ∀ (x : MvPowerSeries σ R), x * φ = 0 → x = 0
Tactic: classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e x φ).symm
  rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
  · rintro ⟨u, _⟩ huv _
    suffices u < e by simp only [he u this, zero_mul, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]
    · rintro rfl
      simp_all
  · simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
intro intro₁ : ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0), x = 0
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsRight (MvPowerSeries σ R)) φ
have h : ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0) (d : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e x φ).symm
  rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
  · rintro ⟨u, _⟩ huv _
    suffices u < e by simp only [he u this, zero_mul, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]
    · rintro rfl
      simp_all
  · simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
intro intro₁ : ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0), x = 0
h :
  ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0) (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsRight (MvPowerSeries σ R)) φ
have h₁ : ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0) (d 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)
Tactic: classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e x φ).symm
  rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
  · rintro ⟨u, _⟩ huv _
    suffices u < e by simp only [he u this, zero_mul, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]
    · rintro rfl
      simp_all
  · simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
intro intro₁ : ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0), x = 0
h :
  ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0) (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
h₁ h₂ :
  ∀ (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) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) 0 : R)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsRight (MvPowerSeries σ R)) φ
have h₃ : ∀ (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)),
  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: classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e x φ).symm
  rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
  · rintro ⟨u, _⟩ huv _
    suffices u < e by simp only [he u this, zero_mul, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]
    · rintro rfl
      simp_all
  · simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
intro intro₁ : ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0), x = 0
h :
  ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0) (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
h₁ h₂ :
  ∀ (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) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) 0 : R)
h₃ :
  ∀ (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)),
    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 * φ)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsRight (MvPowerSeries σ R)) φ
have h₄ : ∀ (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)),
  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: classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e x φ).symm
  rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
  · rintro ⟨u, _⟩ huv _
    suffices u < e by simp only [he u this, zero_mul, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]
    · rintro rfl
      simp_all
  · simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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)
intro intro₁ : ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0), x = 0
h :
  ∀ (x : MvPowerSeries σ R) (hx : x * φ = 0) (d : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
h₁ h₂ :
  ∀ (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) ((coeff e : (a : MvPowerSeries σ R) → R) x : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) 0 : R)
h₃ :
  ∀ (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)),
    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 * φ)
h₄ :
  ∀ (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)),
    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)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsRight (MvPowerSeries σ R)) φ
have h₅ : ∀ (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)),
  ∀ 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
Tactic: classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e x φ).symm
  rw [Finset.sum_eq_single (e, 0), coeff_zero_eq_constantCoeff]
  · rintro ⟨u, _⟩ huv _
    suffices u < e by simp only [he u this, zero_mul, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]
    · rintro rfl
      simp_all
  · simp
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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
⊢ x = 0
have h : ∀ (d : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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 : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) x : R) ((coeff d : (a : MvPowerSeries σ R) → R) 0 : R)
have 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)
Tactic: apply WellFoundedLT.induction d
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
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) ((coeff e : (a : MvPowerSeries σ R) → R) x : R) ((coeff e : (a : MvPowerSeries σ R) → R) 0 : R)
have 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)
Tactic: rw [map_zero, ← mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]