internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case h
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
⊢ ∏ i ∈ range n, (coeff α (k i)) f = 0
Tactic:
set s := (range n).filter fun i => k i = 0 with hs_def
Proof state after:
case h
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
⊢ ∏ i ∈ range n, (coeff α (k i)) f = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case h
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
⊢ s ⊆ range n
Tactic:
apply filter_subset
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
⊢ ∏ i ∈ range n, (coeff α (k i)) f = 0
Tactic:
rw [← prod_sdiff hs]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
⊢ (∏ x ∈ range n \ s, (coeff α (k x)) f) * ∏ x ∈ s, (coeff α (k x)) f = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
⊢ (∏ x ∈ range n \ s, (coeff α (k x)) f) * ∏ x ∈ s, (coeff α (k x)) f = 0
Tactic:
refine' mul_eq_zero_of_right _ _
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
⊢ ∏ x ∈ s, (coeff α (k x)) f = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
⊢ ∏ x ∈ s, (coeff α (k x)) f = 0
Tactic:
have hs' : ∀ i ∈ s, coeff α (k i) f = constantCoeff σ α f := by
  intro i hi
  simp only [hs_def, mem_filter] at hi
  rw [hi.2, coeff_zero_eq_constantCoeff]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ ∏ x ∈ s, (coeff α (k x)) f = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ ∏ x ∈ s, (coeff α (k x)) f = 0
Tactic:
rw [prod_congr rfl hs', prod_const]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ (constantCoeff σ α) f ^ s.card = 0
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ (constantCoeff σ α) f ^ s.card = 0
Tactic:
suffices m ≤ s.card by
  obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
  rw [hm', pow_add, hf, MulZeroClass.zero_mul]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ m ≤ s.card
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ m ≤ s.card
Tactic:
rw [← Nat.add_le_add_iff_right, add_comm s.card, Finset.card_sdiff_add_card_eq_card hs]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ m + (range n \ s).card ≤ (range n).card
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ m + (range n \ s).card ≤ (range n).card
Tactic:
simp only [card_range]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ m + (range n \ s).card ≤ n
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ m + (range n \ s).card ≤ n
Tactic:
apply le_trans _ hn
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ m + (range n \ s).card ≤ m + degree d
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ m + (range n \ s).card ≤ m + degree d
Tactic:
simp only [add_comm m, Nat.add_le_add_iff_right]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ (range n \ s).card ≤ degree d
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ (range n \ s).card ≤ degree d
Tactic:
rw [← hk.2, map_sum, ← sum_sdiff hs]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ (range n \ s).card ≤ ∑ x ∈ range n \ s, degree (k x) + ∑ x ∈ s, degree (k x)
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
⊢ (range n \ s).card ≤ ∑ x ∈ range n \ s, degree (k x) + ∑ x ∈ s, degree (k x)
Tactic:
have hs'' : ∀ i ∈ s, degree (k i) = 0 := by
  intro i hi
  simp only [hs_def, mem_filter] at hi
  rw [hi.2, map_zero]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ (range n \ s).card ≤ ∑ x ∈ range n \ s, degree (k x) + ∑ x ∈ s, degree (k x)
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ (range n \ s).card ≤ ∑ x ∈ range n \ s, degree (k x) + ∑ x ∈ s, degree (k x)
Tactic:
rw [sum_eq_zero hs'', add_zero]
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ (range n \ s).card ≤ ∑ x ∈ range n \ s, degree (k x)
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ (range n \ s).card ≤ ∑ x ∈ range n \ s, degree (k x)
Tactic:
convert Finset.card_nsmul_le_sum (range n \ s) _ 1 _
Proof state after:
case h.e'_3
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ (range n \ s).card = (range n \ s).card • 1

case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
case h.e'_3
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ (range n \ s).card = (range n \ s).card • 1

case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)
Tactic:
simp only [Algebra.id.smul_eq_mul, mul_one]
Proof state after:
case convert_2
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
hs'' : ∀ i ∈ s, degree (k i) = 0
⊢ ∀ x ∈ range n \ s, 1 ≤ degree (k x)
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
⊢ ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
Tactic:
intro i hi
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
i : ℕ
hi : i ∈ s
⊢ (coeff α (k i)) f = (constantCoeff σ α) f
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
i : ℕ
hi : i ∈ s
⊢ (coeff α (k i)) f = (constantCoeff σ α) f
Tactic:
simp only [hs_def, mem_filter] at hi
Proof state after:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ (coeff α (k i)) f = (constantCoeff σ α) f
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ (coeff α (k i)) f = (constantCoeff σ α) f
Tactic:
rw [hi.2, coeff_zero_eq_constantCoeff]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent
Proof state before:
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
this : m ≤ s.card
⊢ (constantCoeff σ α) f ^ s.card = 0
Tactic:
obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
Proof state after:
case intro
σ : Type u_1
inst✝³ : DecidableEq σ
ι : Type u_2
inst✝² : DecidableEq (ι → σ →₀ ℕ)
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq (ℕ → σ →₀ ℕ)
f : MvPowerSeries σ α
m : ℕ
hf : (constantCoeff σ α) f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k.support ⊆ range n ∧ (range n).sum ⇑k = d
s : Finset ℕ := filter (fun i => k i = 0) (range n)
hs_def : s = filter (fun i => k i = 0) (range n)
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff α (k i)) f = (constantCoeff σ α) f
this : m ≤ s.card
m' : ℕ
hm' : s.card = m + m'
⊢ (constantCoeff σ α) f ^ s.card = 0