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
φ : 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)
⊢ 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)
have 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)
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) (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)
⊢ 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)
have 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
Tactic: rw [Finset.sum_eq_single (0, e), 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) (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
⊢ 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)
have 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
Tactic: rw [Finset.sum_eq_single (0, e), 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) (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)
⊢ HMul.hMul (α := R) (β := R) ((coeff (fst, u).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (fst, u).2 : (a : MvPowerSeries σ R) → R) x : R) =
    0
have h : u < e
Tactic: suffices u < e by simp only [he u this, mul_zero, 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) (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
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) (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
⊢ 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) (nonZeroDivisorsLeft R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (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_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e φ x).symm
  rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]
  · rintro ⟨_, u⟩ huv _
    suffices u < e by simp only [he u this, mul_zero, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]
    · rintro rfl
      simp_all
  · simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]
-- 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)
intro intro₁ : ∀ (x : MvPowerSeries σ R) (hx : φ * x = 0), x = 0
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (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_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e φ x).symm
  rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]
  · rintro ⟨_, u⟩ huv _
    suffices u < e by simp only [he u this, mul_zero, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]
    · rintro rfl
      simp_all
  · simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]
-- 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)
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)) (nonZeroDivisorsLeft (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_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e φ x).symm
  rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]
  · rintro ⟨_, u⟩ huv _
    suffices u < e by simp only [he u this, mul_zero, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]
    · rintro rfl
      simp_all
  · simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]
-- 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)
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)) (nonZeroDivisorsLeft (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) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff e : (a : MvPowerSeries σ R) → R) x : 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_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e φ x).symm
  rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]
  · rintro ⟨_, u⟩ huv _
    suffices u < e by simp only [he u this, mul_zero, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]
    · rintro rfl
      simp_all
  · simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]
-- 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)
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) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff e : (a : MvPowerSeries σ R) → R) x : R) =
      (coeff e : (a : MvPowerSeries σ R) → R) (φ * x)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (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) ((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: classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e φ x).symm
  rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]
  · rintro ⟨_, u⟩ huv _
    suffices u < e by simp only [he u this, mul_zero, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]
    · rintro rfl
      simp_all
  · simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]
-- 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)
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) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff e : (a : MvPowerSeries σ R) → R) x : 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) ((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)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisorsLeft (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 ≠ (0, e) →
      HMul.hMul (α := R) (β := R) ((coeff b.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff b.2 : (a : MvPowerSeries σ R) → R) x : R) =
        0
Tactic: classical
  intro x hx
  ext d
  apply WellFoundedLT.induction d
  intro e he
  rw [map_zero, ← mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff hφ,
    ← map_zero (f := coeff e), ← hx]
  convert! (coeff_mul e φ x).symm
  rw [Finset.sum_eq_single (0, e), coeff_zero_eq_constantCoeff]
  · rintro ⟨_, u⟩ huv _
    suffices u < e by simp only [he u this, mul_zero, map_zero]
    apply lt_of_le_of_ne
    · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_left, zero_le]
    · rintro rfl
      simp_all
  · simp only [mem_antidiagonal, zero_add, not_true_eq_false, coeff_zero_eq_constantCoeff,
      false_implies]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
r : 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
have 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
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
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
⊢ 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
have 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)
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)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
    ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : r * s = 0
⊢ HMul.hMul (α := MvPowerSeries σ R) (β := MvPowerSeries σ R)
      ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
      ((C : (a : R) → MvPowerSeries σ R) s : MvPowerSeries σ R) =
    0
have rw : Eq (α := MvPowerSeries σ R) ((monomial (n + 0) : (a : R) → MvPowerSeries σ R) (r * s) : 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)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
    ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : r * s = 0
⊢ Eq (α := MvPowerSeries σ R) ((monomial (n + 0) : (a : R) → MvPowerSeries σ R) (r * s) : MvPowerSeries σ R)
    (0 : MvPowerSeries σ R)
have 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)
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)) (nonZeroDivisorsLeft (MvPowerSeries σ R))
    ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)
s : R
hrs : r * s = 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) (nonZeroDivisorsLeft R) r
p : MvPowerSeries σ R
hrp : HMul.hMul (α := MvPowerSeries σ R) ((monomial n : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R) p = 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) (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 : (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) ((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)
-- 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) (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)
⊢ 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) 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
n : σ →₀ ℕ
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 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
Tactic: constructor