awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
u v : σ →₀ ℕ
insert :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ attach (s.finsuppAntidiag v),
      HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
        (∏ i ∈ s, (coeff (((↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R))
    (∑ x ∈ attach (s.finsuppAntidiag v),
      ∏ x_1 ∈ Insert.insert a s,
        (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
            (a : MvPowerSeries σ R) → R)
          (f x_1))
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R) =
    ∑ x ∈ attach (s.finsuppAntidiag v),
      ∏ x_1 ∈ Insert.insert a s,
        (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
            (a : MvPowerSeries σ R) → R)
          (f x_1)

Tactic:
rw [ih, Finset.mul_sum, ← Finset.sum_attach]

Premises used: Finset.mul_sum, Finset.sum_attach
-- 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)
u v : σ →₀ ℕ
insert :
  ∀ (x : ↥(s.finsuppAntidiag v)),
    Membership.mem (γ := Finset ↥(s.finsuppAntidiag v)) (attach (s.finsuppAntidiag v)) x →
      HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
          (∏ i ∈ s, (coeff (((↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R) =
        ∏ x_1 ∈ Insert.insert a s,
          (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
              (a : MvPowerSeries σ R) → R)
            (f x_1)
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ attach (s.finsuppAntidiag v),
      HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
        (∏ i ∈ s, (coeff (((↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R))
    (∑ x ∈ attach (s.finsuppAntidiag v),
      ∏ x_1 ∈ Insert.insert a s,
        (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
            (a : MvPowerSeries σ R) → R)
          (f x_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)
u v : σ →₀ ℕ
insert :
  ∀ (a_1 : Finsupp.{u_4, u_1} ι (σ →₀ ℕ))
    (b : Membership.mem (γ := Finset (Finsupp.{u_4, u_1} ι (σ →₀ ℕ))) (s.finsuppAntidiag v) a_1),
    HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
        (∏ x ∈ s, (coeff ((a_1 : (a : ι) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) (f x) : R) =
      HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
        (∏ x ∈ s,
            (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑a_1 : (a : ι) → σ →₀ ℕ) a u x) :
                (a : MvPowerSeries σ R) → R)
              (f x) :
          R)
⊢ ∀ (x : ↥(s.finsuppAntidiag v)),
    Membership.mem (γ := Finset ↥(s.finsuppAntidiag v)) (attach (s.finsuppAntidiag v)) x →
      HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
          (∏ i ∈ s, (coeff (((↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R) =
        ∏ x_1 ∈ Insert.insert a s,
          (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
              (a : MvPowerSeries σ R) → R)
            (f x_1)

Tactic:
simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left,
        Subtype.forall]

Premises used: forall_true_left, Finset.prod_insert, Finset.mem_attach, Subtype.forall, Function.update_self
-- 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)
u v : σ →₀ ℕ
x : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
insert :
  ∀ x_1 ∈ s,
    Eq.{u_3 + 1} (α := R) ((coeff ((x : (a : ι) → σ →₀ ℕ) x_1) : (a : MvPowerSeries σ R) → R) (f x_1) : R)
      ((coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑x : (a : ι) → σ →₀ ℕ) a u x_1) :
            (a : MvPowerSeries σ R) → R)
          (f x_1) :
        R)
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
      (∏ x_1 ∈ s, (coeff ((x : (a : ι) → σ →₀ ℕ) x_1) : (a : MvPowerSeries σ R) → R) (f x_1) : R) =
    HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
      (∏ x_1 ∈ s,
          (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑x : (a : ι) → σ →₀ ℕ) a u x_1) :
              (a : MvPowerSeries σ R) → R)
            (f x_1) :
        R)

Tactic:
rw [Finset.prod_congr rfl]

Premises used: Finset.prod_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)
u v : σ →₀ ℕ
x : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
i : ι
hi : i ∈ s
insert : i ≠ a
⊢ Eq.{u_3 + 1} (α := R) ((coeff ((x : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
    ((coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑x : (a : ι) → σ →₀ ℕ) a u i) : (a : MvPowerSeries σ R) → R)
        (f i) :
      R)

Tactic:
rw [Function.update_of_ne]

Premises used: Function.update_of_ne
-- 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)
u v : σ →₀ ℕ
x : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
i : ι
hi : i ∈ s
⊢ i ≠ a

Tactic:
ne_of_mem_of_not_mem hi ha

Premises used: ne_of_mem_of_not_mem
-- 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)
u v : σ →₀ ℕ
x : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
i : ι
hi : i ∈ s
⊢ i ≠ a

Tactic:
exact ne_of_mem_of_not_mem hi ha

Premises used: ne_of_mem_of_not_mem
-- 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 →
      ∀ (a_3 b_1 : σ →₀ ℕ),
        a_3 + b_1 = d →
          (a_1 = a_3 → ¬b = b_1) →
            ∀ (a_6 : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)),
              Membership.mem (γ := Finset (Finsupp.{u_4, u_1} ι (σ →₀ ℕ))) (s.finsuppAntidiag b) a_6 →
                ∀ (x : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)),
                  Membership.mem (γ := Finset (Finsupp.{u_4, u_1} ι (σ →₀ ℕ))) (s.finsuppAntidiag b_1) x →
                    ¬x.update a a_3 = a_6.update a a_1
⊢ (↑(@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))

Tactic:
simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq,
        disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists,
        exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
        Prod.forall, Prod.mk.injEq]

Premises used: and_imp, Set.PairwiseDisjoint, Finset.mem_attach, Subtype.exists, forall_exists_index, not_exists, exists_prop, Set.Pairwise, ne_eq, Finset.HasAntidiagonal.mem_antidiagonal, Prod.mk.injEq, Function.Embedding.coeFn_mk, Prod.forall, Finset.disjoint_left, Finset.mem_map, not_and, Finset.mem_coe, forall_apply_eq_imp_iff₂, true_and
-- 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)
u v u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
hkl : l.update a u' = k.update a u
⊢ u' = u

Tactic:
simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a

Premises used: DFunLike.congr_fun, Finsupp.coe_update, Function.update_self
-- 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)
u v u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
hkl : l.update a u' = k.update a u
⊢ u' + v' = u' + v

Tactic:
obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a

Premises used: 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)
u v u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
hkl : l.update a u' = k.update a u
huv₁ : u' + v' = u' + v
⊢ u' = u' → ¬v = v'

Tactic:
obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a

Premises used: 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)
u v u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
hkl : l.update a u' = k.update a u
huv₁ : u' + v' = u' + v
h₁ : u' = u' → ¬v = v'
⊢ l.update a u' = k.update a u'

Tactic:
obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a

Premises used: 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)
v u' v' : σ →₀ ℕ
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
huv : u' + v' = u' + v
h : u' = u' → ¬v = v'
hkl : l.update a u' = k.update a u'
⊢ v' = v

Tactic:
simp only [add_right_inj] at huv

Premises used: add_right_inj
-- 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)
v u' v' : σ →₀ ℕ
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
h : u' = u' → ¬v = v'
hkl : l.update a u' = k.update a u'
huv : v' = v
⊢ False

Tactic:
h rfl huv.symm

Premises used: Eq.symm, 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)
v u' v' : σ →₀ ℕ
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
h : u' = u' → ¬v = v'
hkl : l.update a u' = k.update a u'
huv : v' = v
⊢ False

Tactic:
exact h rfl huv.symm

Premises used: Eq.symm, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
f : ι → σ →₀ ℕ
g : ι → R
⊢ Eq (α := MvPowerSeries σ R) (∏ i ∈ ∅, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
    ((monomial (∑ i ∈ ∅, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ ∅, g i))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
f : ι → σ →₀ ℕ
g : ι → R
a : ι
s : Finset ι
ha : a ∉ s
h :
  Eq (α := MvPowerSeries σ R) (∏ i ∈ s, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ s, g i))
⊢ Eq (α := MvPowerSeries σ R) (∏ i ∈ cons a s ha, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
    ((monomial (∑ i ∈ cons a s ha, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ cons a s ha, g i))

Tactic:
simp [h, monomial_mul_monomial]

Premises used: MvPowerSeries.monomial_mul_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
f : ι → σ →₀ ℕ
g : ι → R
s : Finset ι
empty :
  Eq (α := MvPowerSeries σ R) (∏ i ∈ ∅, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
    ((monomial (∑ i ∈ ∅, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ ∅, g i))
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (h :
      Eq (α := MvPowerSeries σ R) (∏ i ∈ s, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
        ((monomial (∑ i ∈ s, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ s, g i))),
    Eq (α := MvPowerSeries σ R) (∏ i ∈ Finset.cons a s ha, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
      ((monomial (∑ i ∈ Finset.cons a s ha, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ Finset.cons a s ha, g i))
⊢ Eq (α := MvPowerSeries σ R) (∏ i ∈ s, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ s, g i))

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha h => simp [h, monomial_mul_monomial]

Premises used: Finset.cons, MvPowerSeries.monomial_mul_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
rw :
  Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ x ∈ range n, f) : R)
    (∑ l ∈ (range n).finsuppAntidiag d,
        ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f :
      R)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := R)
    (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
    (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R)
    (∑ l ∈ (range n).finsuppAntidiag d,
        ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f :
      R)

Tactic:
rw [this, coeff_prod]

Premises used: MvPowerSeries.coeff_prod
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
suffices : f ^ n = ∏ x ∈ range n, f
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R)
    (∑ l ∈ (range n).finsuppAntidiag d,
        ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f :
      R)

Tactic:
suffices f ^ n = (Finset.range n).prod fun _ ↦ f by
    rw [this, coeff_prod]
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
rw : f ^ n = f ^ #(range n)
rw₁ rw₂ : f ^ n = f ^ n
⊢ f ^ n = ∏ x ∈ range n, f

Tactic:
rw [Finset.prod_const, card_range]

Premises used: Finset.card_range, Finset.prod_const
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
m : σ →₀ ℕ
a : R
n : ℕ
rw :
  Eq (α := MvPowerSeries σ R) (∏ _k ∈ range n, (monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
rw₁ :
  Eq (α := MvPowerSeries σ R)
    ((monomial (∑ i ∈ range n, m) : (a : R) → MvPowerSeries σ R) (∏ i ∈ range n, a) : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
rw₂ :
  Eq (α := MvPowerSeries σ R) ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (∏ i ∈ range n, a) : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
rw₃ rw₄ :
  Eq (α := MvPowerSeries σ R) ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
⊢ HPow.hPow (α := MvPowerSeries σ R) ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) n =
    (monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n)

Tactic:
rw [Finset.pow_eq_prod_const, prod_monomial, ← Finset.nsmul_eq_sum_const,
    ← Finset.pow_eq_prod_const]

Premises used: Finset.nsmul_eq_sum_const, Finset.pow_eq_prod_const, MvPowerSeries.prod_monomial
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
rw :
  Eq.{u_3 + 1} (α := R)
    (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
    0
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R) (0 : R)

Tactic:
rw [coeff_pow]

Premises used: MvPowerSeries.coeff_pow
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
h :
  ∀ (x : ℕ →₀ σ →₀ ℕ),
    Membership.mem (γ := Finset (ℕ →₀ σ →₀ ℕ)) ((range n).finsuppAntidiag d) x →
      Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((x : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
⊢ Eq.{u_3 + 1} (α := R)
    (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
    0

Tactic:
apply sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : Membership.mem (γ := Finset (ℕ →₀ σ →₀ ℕ)) ((range n).finsuppAntidiag d) k
⊢ (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n

Tactic:
rw [mem_finsuppAntidiag] at hk

Premises used: Finset.mem_finsuppAntidiag
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
⊢ let s := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)};
  s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}

Tactic:
set s := {i ∈ range n | k i = 0} with hs_def

Premises used: Finset.range
-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
⊢ s ⊆ range n

Tactic:
have hs : s ⊆ range n := filter_subset _ _