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
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 :
  (∀ (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:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : (m : (a : σ) → ℕ) s < n
mp :
  ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R)
        ((coeff x.1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R) =
      0
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n * φ) : R)
    (0 : R)

Tactic:
rw [coeff_mul, Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero, MvPowerSeries.coeff_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : (m : (a : σ) → ℕ) s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
mp : ¬(i, j).1 = single s n
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) φ : R) =
    0

Tactic:
rw [coeff_X_pow, if_neg, zero_mul]

Premises used: MvPowerSeries.coeff_X_pow, MulZeroClass.zero_mul, if_neg
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : (m : (a : σ) → ℕ) s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
mp : ∀ (h : (i, j).1 = single s n), n ≤ (m : (a : σ) → ℕ) s
⊢ ¬(i, j).1 = single 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
m i j : σ →₀ ℕ
hij : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
h : i = single s n
⊢ (single s n, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m

Tactic:
subst i
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ (single s n, j).1 + (single s n, j).2 = m

Tactic:
rw [mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
mp : n ≤ HAdd.hAdd (β := ℕ) n (((single s n, j).2 : (a : σ) → ℕ) s : ℕ)
⊢ n ≤ (m : (a : σ) → ℕ) s

Tactic:
rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, Finsupp.add_apply
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ HAdd.hAdd (β := ℕ) n (((single s n, j).2 : (a : σ) → ℕ) s : ℕ)

Tactic:
Nat.le_add_right n _

Premises used: Nat.le_add_right
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ HAdd.hAdd (β := ℕ) n (((single s n, j).2 : (a : σ) → ℕ) s : ℕ)

Tactic:
exact Nat.le_add_right n _

Premises used: Nat.le_add_right
-- 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)
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ

Tactic:
⟨fun m => coeff (m + single s n) φ, ?_⟩

Premises used: HAdd.hAdd, MvPowerSeries.coeff, Exists.intro, DFunLike.coe, Finsupp.single
-- 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)
mpr :
  φ =
    HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
      (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ

Tactic:
refine ⟨fun m => coeff (m + single s n) φ, ?_⟩
-- 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)
mpr :
  ∀ (m : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
        R)
⊢ φ =
    HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
      (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ

Tactic:
ext m
-- 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 : σ →₀ ℕ
pos :
  ∀ (H : m - single s n + single s n = m),
    Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
        R)
neg :
  ∀ (H : ¬m - single s n + single s n = m),
    Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
        R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)

Tactic:
by_cases H : m - single s n + single s n = m

Premises used: Finsupp.single
-- 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
pos :
  (coeff m : (a : MvPowerSeries σ R) → R) φ =
    HMul.hMul (α := R) (β := R)
      ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
        R)
      ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R)
pos₁ :
  ∀ b ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    b ≠ (single s n, m - single s n) →
      HMul.hMul (α := R) (β := R)
          ((coeff b.1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
          ((coeff b.2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
              (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
            R) =
        0
pos₂ :
  (single s n, m - single s n) ∉ @antidiagonal _ Finsupp.instAddMonoid _ m →
    HMul.hMul (α := R) (β := R)
        ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R)
            (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
          R)
        ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
          R) =
      0
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)

Tactic:
rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]

Premises used: HSub.hSub, Prod.mk, Finset.sum_eq_single, MvPowerSeries.coeff_mul, Finsupp.single
-- 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
pos :
  Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
        (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
      R)
⊢ (coeff m : (a : MvPowerSeries σ R) → R) φ =
    HMul.hMul (α := R) (β := R)
      ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
        R)
      ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R)

Tactic:
rw [coeff_X_pow, if_pos rfl, one_mul]

Premises used: MvPowerSeries.coeff_X_pow, if_pos, one_mul, rfl
-- 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
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
        (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
      R)

Tactic:
simpa using congr_arg (fun m : σ →₀ ℕ => coeff m φ) H.symm

Premises used: congr_arg, MvPowerSeries.coeff, Eq.symm, DFunLike.coe
-- 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) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ (i, j).1 + (i, j).2 = m

Tactic:
rw [mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
hne : (i, j) ≠ (single s n, m - single s n)
hij₁ : (i, j).1 + (i, j).2 = m
⊢ (i, j) ≠ (single s n, m - single s n)

Tactic:
rw [mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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
hne : (i, j) ≠ (single s n, m - single s n)
pos :
  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
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0

Tactic:
rw [coeff_X_pow]

Premises used: MvPowerSeries.coeff_X_pow
-- 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
hne : (i, j) ≠ (single s n, m - single s n)
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
hne : (i, j) ≠ (single s n, m - single s n)
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
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
pos : (i, j) = (single s n, m - single s n)
⊢ False

Tactic:
apply hne
-- 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
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
pos : i = (i, j).1 ∧ j = (i, j).1 + (i, j).2 - (i, j).1
⊢ (i, j) = (single s n, m - single s n)

Tactic:
rw [← hij, ← hi, Prod.mk_inj]

Premises used: Prod.mk_inj
-- 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
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ i = (i, j).1 ∧ j = (i, j).1 + (i, j).2 - (i, j).1

Tactic:
⟨rfl, ?_⟩

Premises used: And.intro, rfl
-- 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
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
pos : j = (i, j).1 + (i, j).2 - (i, j).1
⊢ i = (i, j).1 ∧ j = (i, j).1 + (i, j).2 - (i, j).1

Tactic:
refine ⟨rfl, ?_⟩
-- 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
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
pos : ∀ (t : σ), Eq (α := ℕ) ((j : (a : σ) → ℕ) t : ℕ) (((i, j).1 + (i, j).2 - (i, j).1 : (a : σ) → ℕ) t : ℕ)
⊢ j = (i, j).1 + (i, j).2 - (i, j).1

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 : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
t : σ
⊢ Eq (α := ℕ) ((j : (a : σ) → ℕ) t : ℕ) (((i, j).1 + (i, j).2 - (i, j).1 : (a : σ) → ℕ) t : ℕ)

Tactic:
simp only [add_tsub_cancel_left]

Premises used: add_tsub_cancel_left
-- 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
hne : (i, j) ≠ (single s n, m - single s n)
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
hne : (i, j) ≠ (single s n, m - single s n)
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
hni : (single s n, m - single s n) ∉ @antidiagonal _ Finsupp.instAddMonoid _ m
pos : False
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
        R)
      ((coeff (single s n, m - single s n).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
hni : (single s n, m - single s n) ∉ @antidiagonal _ Finsupp.instAddMonoid _ m
pos : (single s n, m - single s n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ False

Tactic:
apply hni
-- 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
hni : (single s n, m - single s n) ∉ @antidiagonal _ Finsupp.instAddMonoid _ m
pos : (single s n, m - single s n).1 + (single s n, m - single s n).2 = m
pos₁ pos₂ pos₃ pos₄ : (single s n, m - single s n).2 + (single s n, m - single s n).1 = m
⊢ (single s n, m - single s n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m

Tactic:
rwa [mem_antidiagonal, add_comm]

Premises used: add_comm, Finset.HasAntidiagonal.mem_antidiagonal
-- 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 :
  ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    HMul.hMul (α := R) (β := R)
        ((coeff x.1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
          R) =
      0
neg₁ : (m : (a : σ) → ℕ) s < n
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)

Tactic:
rw [h, coeff_mul, Finset.sum_eq_zero]

Premises used: Finset.sum_eq_zero, MvPowerSeries.coeff_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) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ (i, j).1 + (i, j).2 = m

Tactic:
rw [mem_antidiagonal] at hij

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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
neg :
  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
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0

Tactic:
rw [coeff_X_pow]

Premises used: MvPowerSeries.coeff_X_pow