Theorem: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent (DividedPowers/ForMathlib/MvPowerSeries/Basic.lean)

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
⊢ (coeff α d) (f ^ n) = 0
Tactic:
rw [coeff_pow]
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
⊢ ∑ l ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (l i)) f = 0

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
⊢ ∑ l ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (l i)) f = 0
Tactic:
apply sum_eq_zero
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
⊢ ∀ x ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (x i)) f = 0

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
⊢ ∀ x ∈ (range n).piAntidiagonal d, ∏ i ∈ range n, (coeff α (x i)) f = 0
Tactic:
intro k hk
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 ∈ (range n).piAntidiagonal d
⊢ ∏ i ∈ range n, (coeff α (k i)) f = 0

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 ∈ (range n).piAntidiagonal d
⊢ ∏ i ∈ range n, (coeff α (k i)) f = 0
Tactic:
rw [mem_piAntidiagonal'] at hk
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
⊢ ∏ i ∈ range n, (coeff α (k i)) f = 0

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
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

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
State after:
no goals

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]
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

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 _ _
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

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]
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

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]
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

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]
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

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]
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

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]
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

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
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

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]
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

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]
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)

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]
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)

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]
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)

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 _
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)

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]
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)

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
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

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
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

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]
State after:
no goals

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
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

State before:
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
Tactic:
rw [hm', pow_add, hf, MulZeroClass.zero_mul]
State after:
no goals

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
⊢ ∀ i ∈ s, degree (k i) = 0
Tactic:
intro i hi
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
i : ℕ
hi : i ∈ s
⊢ degree (k i) = 0

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
i : ℕ
hi : i ∈ s
⊢ degree (k i) = 0
Tactic:
simp only [hs_def, mem_filter] at hi
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
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ degree (k i) = 0

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
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ degree (k i) = 0
Tactic:
rw [hi.2, map_zero]
State after:
no goals

State before:
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 [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
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 < n, (x < n → ¬k x = 0) → 1 ≤ degree (k x)

State before:
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 < n, (x < n → ¬k x = 0) → 1 ≤ degree (k x)
Tactic:
intro i hi hi'
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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ 1 ≤ degree (k i)

State before:
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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ 1 ≤ degree (k i)
Tactic:
rw [← not_lt]
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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ ¬degree (k i) < 1

State before:
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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
⊢ ¬degree (k i) < 1
Tactic:
intro h
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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
h : degree (k i) < 1
⊢ False

State before:
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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
h : degree (k i) < 1
⊢ False
Tactic:
apply hi' hi
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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
h : degree (k i) < 1
⊢ k i = 0

State before:
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
i : ℕ
hi : i < n
hi' : i < n → ¬k i = 0
h : degree (k i) < 1
⊢ k i = 0
Tactic:
simpa only [Nat.lt_one_iff, degree_eq_zero_iff] using h
State after:
no goals