awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
i : ℕ
hi : i ∈ s
⊢ i ∈ range n ∧ Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)

Tactic:
simp only [hs_def, mem_filter] at hi

Premises used: Finset.mem_filter
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
i : ℕ
hi : i ∈ range n ∧ Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
rw :
  Eq.{u_3 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) f : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
rw [hi.2, coeff_zero_eq_constantCoeff]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff, And.right
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
⊢ ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
have hs' (i : ℕ) (hi : i ∈ s) : coeff (k i) f = constantCoeff f := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2, coeff_zero_eq_constantCoeff]
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
i : ℕ
hi : i ∈ s
⊢ i ∈ range n ∧ Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)

Tactic:
simp only [hs_def, mem_filter] at hi

Premises used: Finset.mem_filter
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
i : ℕ
hi : i ∈ range n ∧ Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
rw rw₁ : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
⊢ Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)

Tactic:
rw [hi.2]

Premises used: And.right
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)

Tactic:
have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 := by
    simp only [hs_def, mem_filter] at hi
    rw [hi.2]
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
h :
  HMul.hMul (α := R) (∏ x ∈ range n \ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) f)
      (∏ x ∈ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) f) =
    0
⊢ Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0

Tactic:
rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]

Premises used: Finset.filter_subset, Finset.prod_sdiff
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
h : Eq.{u_3 + 1} (α := R) (∏ x ∈ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) f) 0
⊢ HMul.hMul (α := R) (∏ x ∈ range n \ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) f)
      (∏ x ∈ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) f) =
    0

Tactic:
apply mul_eq_zero_of_right

Premises used: mul_eq_zero_of_right
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
h : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
⊢ Eq.{u_3 + 1} (α := R) (∏ x ∈ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) f) 0

Tactic:
rw [prod_congr rfl hs', prod_const]

Premises used: Finset.prod_congr, Finset.prod_const, rfl
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
this : m ≤ #s
obtain : ∀ (m' : ℕ) (hm' : #s = m + m'), HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
⊢ HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0

Tactic:
obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this

Premises used: Nat.exists_eq_add_of_le
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
this : m ≤ #s
m' : ℕ
hm' : #s = m + m'
rw : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (m + m') = 0
rw₁ :
  HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m *
      HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m' =
    0
rw₂ : 0 * HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m' = 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := R) 0 0
⊢ HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0

Tactic:
rw [hm', pow_add, hf, zero_mul]

Premises used: MulZeroClass.zero_mul, pow_add
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
h : m ≤ #s
⊢ HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0

Tactic:
suffices m ≤ #s by
    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
    rw [hm', pow_add, hf, zero_mul]
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
h : m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤ n
⊢ m ≤ #s

Tactic:
rw [← Nat.add_le_add_iff_right, add_comm #s,
    Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]

Premises used: Nat.add_le_add_iff_right, Finset.card_range, Finset.filter_subset, add_comm, Finset.card, Finset.card_sdiff_add_card_eq_card
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
apply :
  m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤
    HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ)
⊢ m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤ n

Tactic:
apply le_trans _ hn

Premises used: le_trans
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
simp :
  #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤
    (degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x)
⊢ m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤
    HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ)

Tactic:
simp only [add_comm m, Nat.add_le_add_iff_right, ← hk.1,
    ← sum_sdiff (hs), sum_eq_zero (s := s) hs'', add_zero]

Premises used: Nat.add_le_add_iff_right, Finset.sum_eq_zero, add_comm, And.left, add_zero, Finset.sum_sdiff
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
rw : #(range n \ s) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x)
⊢ #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤
    (degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x)

Tactic:
rw [← hs_def]
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
⊢ HSMul.hSMul (β := ℕ) (#(range n \ s)) 1 ≤
    ∑ x ∈ range n \ s, (degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ)

Tactic:
Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _

Premises used: Finsupp.degree, Finset.card_nsmul_le_sum, Finset.range, SDiff.sdiff, OfNat.ofNat, DFunLike.coe
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
h : #(range n \ s) = HSMul.hSMul (β := ℕ) (#(range n \ s)) 1
h₁ :
  Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x) : ℕ)
    (∑ x ∈ range n \ s, (degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)
convert! :
  ∀ x ∈ range n \ s,
    LE.le (α := ℕ) 1 ((fun (x : ℕ) ↦ ((degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)) x)
⊢ #(range n \ s) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x)

Tactic:
convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _

Premises used: Finsupp.degree, Finset.card_nsmul_le_sum, Finset.range, SDiff.sdiff, OfNat.ofNat, DFunLike.coe
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
⊢ #(range n \ s) = HSMul.hSMul (β := ℕ) (#(range n \ s)) 1

Tactic:
simp only [smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one
-- 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 : σ →₀ ℕ)}
hs : s ⊆ range n
hs' :
  ∀ (i : ℕ) (hi : i ∈ s),
    Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
      ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
hs'' : ∀ (i : ℕ) (hi : i ∈ s), Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
⊢ Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x) : ℕ)
    (∑ x ∈ range n \ s, (degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)

Tactic:
simp only [degree_eq_weight_one, map_sum]

Premises used: Finsupp.degree_eq_weight_one, map_sum