awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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)
⊢ Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
have rw₁ : Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
  ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
Tactic: rw [hi.2, coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
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
⊢ Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
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 : σ →₀ ℕ)
have hi₁ : i ∈ range n ∧ Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
Tactic: simp only [hs_def, mem_filter] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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 : σ →₀ ℕ)
⊢ Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
have rw : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
Tactic: rw [hi.2]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
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)
⊢ Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
have hs'' : ∀ (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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
have 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
Tactic: rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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 : σ →₀ ℕ)
⊢ 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
have h : Eq.{u_3 + 1} (α := R) (∏ x ∈ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) f) 0
Tactic: apply mul_eq_zero_of_right
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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.{u_3 + 1} (α := R) (∏ x ∈ s, (coeff ((k : (a : ℕ) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) f) 0
have h : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
Tactic: rw [prod_congr rfl hs', prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
have obtain : ∀ (m' : ℕ) (hm' : #s = m + m'), HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
Tactic: obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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'
⊢ HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
have rw : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (m + m') = 0
Tactic: rw [hm', pow_add, hf, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
have rw₁ : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m *
    HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m' =
  0
Tactic: rw [hm', pow_add, hf, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
have rw₂ : 0 * HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m' = 0
Tactic: rw [hm', pow_add, hf, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
have rw₃ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [hm', pow_add, hf, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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 : σ →₀ ℕ)
⊢ HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) #s = 0
have h : m ≤ #s
Tactic: suffices m ≤ #s by
    obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
    rw [hm', pow_add, hf, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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 : σ →₀ ℕ)
⊢ m ≤ #s
have h : m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤ n
Tactic: rw [← Nat.add_le_add_iff_right, add_comm #s,
    Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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 : σ →₀ ℕ)
⊢ m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤ n
have apply : m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤
  HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ)
Tactic: apply le_trans _ hn
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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 : σ →₀ ℕ)
⊢ m + #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤
    HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ)
have simp : #(range n \ {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}) ≤
  (degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x)
have h : #(range n \ s) = HSMul.hSMul (β := ℕ) (#(range n \ s)) 1
Tactic: convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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
⊢ #(range n \ s) ≤ (degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x)
have h₁ : Eq (α := ℕ) ((degree : (a : σ →₀ ℕ) → ℕ) (∑ x ∈ range n \ s, (k : (a : ℕ) → σ →₀ ℕ) x) : ℕ)
  (∑ x ∈ range n \ s, (degree : (a : σ →₀ ℕ) → ℕ) ((k : (a : ℕ) → σ →₀ ℕ) x : σ →₀ ℕ) : ℕ)
Tactic: convert! Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _