awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
pos :
  ∀ (hi : (i, j).1 = single s n),
    HMul.hMul (α := R) (β := R) (1 : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
          R) =
      0
neg :
  ∀ (hi : ¬(i, j).1 = single s n),
    HMul.hMul (α := R) (β := R) (0 : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
          R) =
      0
⊢ HMul.hMul (α := R) (β := R) (if (i, j).1 = single s n then 1 else 0 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0

Tactic:
split_ifs with hi
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
pos : False
⊢ HMul.hMul (α := R) (β := R) (1 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0

Tactic:
exfalso
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
pos : m - single s n + single s n = m
⊢ False

Tactic:
apply H
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
pos : single s n + (i, j).2 - single s n + single s n = single s n + (i, j).2
⊢ m - single s n + single s n = m

Tactic:
rw [← hij, hi]
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
pos :
  ∀ (a : σ),
    Eq (α := ℕ) ((single s n + (i, j).2 - single s n + single s n : (a : σ) → ℕ) a : ℕ)
      ((single s n + (i, j).2 : (a : σ) → ℕ) a : ℕ)
⊢ single s n + (i, j).2 - single s n + single s n = single s n + (i, j).2

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : (i, j).1 = single s n
a : σ
pos :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    (single s n + (i, j).2 : (a : σ) → ℕ) a
pos₁ :
  HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n + (i, j).2 - single s n) : (a : σ) → ℕ)
      (⇑(single s n) : (a : σ) → ℕ) a =
    HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
pos₂ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n + (i, j).2 - single s n : (a : σ) → ℕ) a : ℕ)
      ((single s n : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := (a : σ) → ℕ) (β := (a : σ) → ℕ) (⇑(single s n) : (a : σ) → ℕ) (⇑(i, j).2 : (a : σ) → ℕ) a
pos₃ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n + (i, j).2 - single s n : (a : σ) → ℕ) a : ℕ)
      ((single s n : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ)
pos₄ :
  HAdd.hAdd (α := ℕ) (β := ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ)
pos₅ pos₆ :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((single s n : (a : σ) → ℕ) a : ℕ) (((i, j).2 : (a : σ) → ℕ) a : ℕ)
⊢ Eq (α := ℕ) ((single s n + (i, j).2 - single s n + single s n : (a : σ) → ℕ) a : ℕ)
    ((single s n + (i, j).2 : (a : σ) → ℕ) a : ℕ)

Tactic:
rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]

Premises used: add_tsub_cancel_left, add_comm, Pi.add_apply, Finsupp.coe_add
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : ¬(i, j).1 = single s n
⊢ HMul.hMul (α := R) (β := R) (0 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0

Tactic:
zero_mul _

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : ¬(i, j).1 = single s n
⊢ HMul.hMul (α := R) (β := R) (0 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0

Tactic:
exact zero_mul _

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : ¬m - single s n + single s n = m
neg : ∀ (H : n ≤ (m : (a : σ) → ℕ) s), m - single s n + single s n = m
⊢ (m : (a : σ) → ℕ) s < n

Tactic:
contrapose! H
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : n ≤ (m : (a : σ) → ℕ) s
neg : ∀ (t : σ), Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
⊢ m - single s n + single s n = m

Tactic:
ext t
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : n ≤ (m : (a : σ) → ℕ) s
t : σ
pos : ∀ (hst : s = t), Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
neg : ∀ (hst : ¬s = t), Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
⊢ Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)

Tactic:
by_cases hst : s = t
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : n ≤ (m : (a : σ) → ℕ) s
t : σ
hst : s = t
pos : Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) s : ℕ) ((m : (a : σ) → ℕ) s : ℕ)
⊢ Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)

Tactic:
subst t
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : n ≤ (m : (a : σ) → ℕ) s
⊢ Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) s : ℕ) ((m : (a : σ) → ℕ) s : ℕ)

Tactic:
simpa using tsub_add_cancel_of_le H

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : n ≤ (m : (a : σ) → ℕ) s
t : σ
hst : ¬s = t
⊢ Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)

Tactic:
simp [hst]
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
mp :
  HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ →
    ∀ (m : σ →₀ ℕ),
      (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
mpr mpr₁ :
  (∀ (m : σ →₀ ℕ),
      (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) →
    HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ ↔
    ∀ (m : σ →₀ ℕ),
      (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
classical
  constructor
  · rintro ⟨φ, rfl⟩ m h
    rw [coeff_mul, Finset.sum_eq_zero]
    rintro ⟨i, j⟩ hij
    rw [coeff_X_pow, if_neg, zero_mul]
    contrapose! h
    dsimp at h
    subst i
    rw [mem_antidiagonal] at hij
    rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]
    exact Nat.le_add_right n _
  · intro h
    refine ⟨fun m => coeff (m + single s n) φ, ?_⟩
    ext m
    by_cases H : m - single s n + single s n = m
    · rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
      · rw [coeff_X_pow, if_pos rfl, one_mul]
        simpa using congr_arg (fun m : σ →₀ ℕ => coeff m φ) H.symm
      · rintro ⟨i, j⟩ hij hne
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply hne
          rw [← hij, ← hi, Prod.mk_inj]
          refine ⟨rfl, ?_⟩
          ext t
          simp only [add_tsub_cancel_left]
        · exact zero_mul _
      · intro hni
        exfalso
        apply hni
        rwa [mem_antidiagonal, add_comm]
    · rw [h, coeff_mul, Finset.sum_eq_zero]
      · rintro ⟨i, j⟩ hij
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply H
          rw [← hij, hi]
          ext
          rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
        · exact zero_mul _
      · contrapose! H
        ext t
        by_cases hst : s = t
        · subst t
          simpa using tsub_add_cancel_of_le H
        · simp [hst]

Premises used: MvPowerSeries.coeff_X_pow, Finsupp.single_eq_same, MulZeroClass.zero_mul, Finset.sum_eq_zero, Nat.le_add_right, Prod.mk_inj, Finsupp.add_apply, add_tsub_cancel_left, if_pos, add_comm, Pi.add_apply, Finsupp.coe_add, Finset.HasAntidiagonal.mem_antidiagonal, if_neg, one_mul, rfl, MvPowerSeries.coeff_mul, Finsupp.single
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
φ : MvPowerSeries σ R
rw :
  (∀ (m : σ →₀ ℕ),
      LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) ↔
    ∀ (m : σ →₀ ℕ),
      Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ X s ∣ φ ↔
    ∀ (m : σ →₀ ℕ),
      Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
rw [← pow_one (X s : MvPowerSeries σ R), X_pow_dvd_iff]

Premises used: MvPowerSeries.X_pow_dvd_iff, MvPowerSeries.X, pow_one
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
φ : MvPowerSeries σ R
mp :
  (∀ (m : σ →₀ ℕ),
      LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) →
    ∀ (m : σ →₀ ℕ),
      Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
mpr :
  (∀ (m : σ →₀ ℕ),
      Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) →
    ∀ (m : σ →₀ ℕ),
      LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ (∀ (m : σ →₀ ℕ),
      LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) ↔
    ∀ (m : σ →₀ ℕ),
      Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
      Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
h m (hm.symm ▸ zero_lt_one)

Premises used: Eq.rec, zero_lt_one, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
      Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ)
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
exact h m (hm.symm ▸ zero_lt_one)

Premises used: Eq.rec, zero_lt_one, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
      Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
hm : LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ)
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
h m (Nat.eq_zero_of_le_zero <| Nat.le_of_succ_le_succ hm)

Premises used: Nat.le_of_succ_le_succ, Nat.eq_zero_of_le_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
      Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
hm : LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ)
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)

Tactic:
exact h m (Nat.eq_zero_of_le_zero <| Nat.le_of_succ_le_succ hm)

Premises used: Nat.le_of_succ_le_succ, Nat.eq_zero_of_le_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
empty :
  Eq.{u_3 + 1} (α := R) (if d = 0 then 1 else 0)
    (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) (if d = 0 then {0} else ∅)) : R)
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ ∅, f j) : R)
    (∑ l ∈ finsuppAntidiag ∅ d, ∏ i ∈ ∅, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)

Tactic:
simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, finsuppAntidiag_empty]

Premises used: Finset.prod_empty, MvPowerSeries.coeff_one, Finset.finsuppAntidiag_empty, nsmul_eq_mul, mul_one, Finset.sum_const
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
pos : d = 0 → Eq.{u_3 + 1} (α := R) 1 (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) {0}) : R)
neg : ¬d = 0 → Eq.{u_3 + 1} (α := R) 0 (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) ∅) : R)
⊢ Eq.{u_3 + 1} (α := R) (if d = 0 then 1 else 0)
    (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) (if d = 0 then {0} else ∅)) : R)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h : d = 0
⊢ Eq.{u_3 + 1} (α := R) 1 (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) {0}) : R)

Tactic:
simp only [card_singleton, Nat.cast_one]

Premises used: Nat.cast_one, Finset.card_singleton
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h : ¬d = 0
⊢ Eq.{u_3 + 1} (α := R) 0 (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) ∅) : R)

Tactic:
simp only [card_empty, Nat.cast_zero]

Premises used: Finset.card_empty, Nat.cast_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
d : σ →₀ ℕ
insert :
  Eq.{u_3 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ d,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) (f a) : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R))
    (∑ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ d,
      ∑
        i ∈
          Finset.map (α := ↥(s.finsuppAntidiag x.2))
            { toFun := fun (f : ↥(s.finsuppAntidiag x.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a x.1, inj' := ⋯ }
            (attach (s.finsuppAntidiag x.2)),
        ∏ i_1 ∈ Insert.insert a s, (coeff ((i : (a : ι) → σ →₀ ℕ) i_1) : (a : MvPowerSeries σ R) → R) (f i_1))
insert₁ :
  (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ d) : Set ((σ →₀ ℕ) × (σ →₀ ℕ))).PairwiseDisjoint (α :=
    Finset (Finsupp.{u_4, u_1} ι (σ →₀ ℕ))) fun (p : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦
    Finset.map (α := ↥(s.finsuppAntidiag p.2))
      { toFun := fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a p.1, inj' := ⋯ }
      (attach (s.finsuppAntidiag p.2))
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ Insert.insert a s, f j) : R)
    (∑ l ∈ (Insert.insert a s).finsuppAntidiag d,
        ∏ i ∈ Insert.insert a s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) :
      R)

Tactic:
rw [finsuppAntidiag_insert ha, prod_insert ha, coeff_mul, sum_biUnion]

Premises used: Finset.prod_insert, Finset.sum_biUnion, Finset.finsuppAntidiag_insert, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
d : σ →₀ ℕ
insert :
  ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ d,
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) (f a) : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R) =
      ∑
        i ∈
          Finset.map (α := ↥(s.finsuppAntidiag x.2))
            { toFun := fun (f : ↥(s.finsuppAntidiag x.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a x.1, inj' := ⋯ }
            (attach (s.finsuppAntidiag x.2)),
        ∏ i_1 ∈ Insert.insert a s, (coeff ((i : (a : ι) → σ →₀ ℕ) i_1) : (a : MvPowerSeries σ R) → R) (f i_1)
⊢ Eq.{u_3 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ d,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) (f a) : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R))
    (∑ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ d,
      ∑
        i ∈
          Finset.map (α := ↥(s.finsuppAntidiag x.2))
            { toFun := fun (f : ↥(s.finsuppAntidiag x.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a x.1, inj' := ⋯ }
            (attach (s.finsuppAntidiag x.2)),
        ∏ i_1 ∈ Insert.insert a s, (coeff ((i : (a : ι) → σ →₀ ℕ) i_1) : (a : MvPowerSeries σ R) → R) (f i_1))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
d : σ →₀ ℕ
insert :
  ∀ (a_1 b : σ →₀ ℕ),
    a_1 + b = d →
      HMul.hMul (α := R) (β := R) ((coeff a_1 : (a : MvPowerSeries σ R) → R) (f a) : R)
          ((coeff b : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R) =
        ∑ x ∈ attach (s.finsuppAntidiag b),
          ∏ x_1 ∈ Insert.insert a s,
            (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a a_1 x_1) :
                (a : MvPowerSeries σ R) → R)
              (f x_1)
⊢ ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ d,
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) (f a) : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R) =
      ∑
        i ∈
          Finset.map (α := ↥(s.finsuppAntidiag x.2))
            { toFun := fun (f : ↥(s.finsuppAntidiag x.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a x.1, inj' := ⋯ }
            (attach (s.finsuppAntidiag x.2)),
        ∏ i_1 ∈ Insert.insert a s, (coeff ((i : (a : ι) → σ →₀ ℕ) i_1) : (a : MvPowerSeries σ R) → R) (f i_1)

Tactic:
simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]

Premises used: Finset.sum_map, Finsupp.coe_update, Finset.HasAntidiagonal.mem_antidiagonal, Function.Embedding.coeFn_mk, Prod.forall