internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.tendsto_pow_zero_of_constantCoeff_nilpotent
Proof state before:
case intro
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
m : ℕ
hm : (constantCoeff σ α) f ^ m = 0
⊢ ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f ^ i)) Filter.atTop (nhds 0)
Tactic:
exact fun d =>  tendsto_atTop_of_eventually_const fun n hn =>
  coeff_eq_zero_of_constantCoeff_nilpotent f m hm d n hn
Proof state after:
no goals
Theorem: MvPowerSeries.tendsto_pow_zero_of_constantCoeff_zero
Proof state before:
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
Tactic:
apply tendsto_pow_zero_of_constantCoeff_nilpotent
Proof state after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_zero_of_constantCoeff_zero
Proof state before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
rw [hf]
Proof state after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ IsNilpotent 0
Theorem: MvPowerSeries.tendsto_pow_zero_of_constantCoeff_zero
Proof state before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ IsNilpotent 0
Tactic:
exact IsNilpotent.zero
Proof state after:
no goals
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0) ↔ IsNilpotent ((constantCoeff σ α) f)
Tactic:
refine' ⟨_, tendsto_pow_zero_of_constantCoeff_nilpotent ⟩
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0) → IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0) → IsNilpotent ((constantCoeff σ α) f)
Tactic:
intro h
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
suffices Filter.Tendsto (fun n : ℕ => constantCoeff σ α (f ^ n)) Filter.atTop (nhds 0) by
  simp only [Filter.tendsto_def] at this
  specialize this {0} _
  suffices  ∀ x : α, {x} ∈ nhds x by exact this 0
  rw [← discreteTopology_iff_singleton_mem_nhds]; infer_instance
  simp only [map_pow, Filter.mem_atTop_sets, ge_iff_le, Set.mem_preimage,
    Set.mem_singleton_iff] at this
  obtain ⟨m, hm⟩ := this
  use m
  apply hm m (le_refl m)
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (constantCoeff σ α) (f ^ n)) Filter.atTop (nhds 0)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (constantCoeff σ α) (f ^ n)) Filter.atTop (nhds 0)
Tactic:
simp only [← @comp_apply _ α ℕ]
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (⇑(constantCoeff σ α) ∘ HPow.hPow f) n) Filter.atTop (nhds 0)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (⇑(constantCoeff σ α) ∘ HPow.hPow f) n) Filter.atTop (nhds 0)
Tactic:
rw [← Filter.tendsto_map'_iff]
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (⇑(constantCoeff σ α)) (Filter.map (HPow.hPow f) Filter.atTop) (nhds 0)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (⇑(constantCoeff σ α)) (Filter.map (HPow.hPow f) Filter.atTop) (nhds 0)
Tactic:
simp only [Filter.Tendsto, Filter.map_le_iff_le_comap] at h ⊢
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.atTop ≤ Filter.comap (HPow.hPow f) (Filter.comap (⇑(constantCoeff σ α)) (nhds 0))
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.atTop ≤ Filter.comap (HPow.hPow f) (Filter.comap (⇑(constantCoeff σ α)) (nhds 0))
Tactic:
apply le_trans h
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.comap (fun n => f ^ n) (nhds 0) ≤ Filter.comap (HPow.hPow f) (Filter.comap (⇑(constantCoeff σ α)) (nhds 0))
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.comap (fun n => f ^ n) (nhds 0) ≤ Filter.comap (HPow.hPow f) (Filter.comap (⇑(constantCoeff σ α)) (nhds 0))
Tactic:
apply Filter.comap_mono
Proof state after:
case a
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ nhds 0 ≤ Filter.comap (⇑(constantCoeff σ α)) (nhds 0)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
case a
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ nhds 0 ≤ Filter.comap (⇑(constantCoeff σ α)) (nhds 0)
Tactic:
rw [← Filter.map_le_iff_le_comap]
Proof state after:
case a
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.map (⇑(constantCoeff σ α)) (nhds 0) ≤ nhds 0
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
case a
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.map (⇑(constantCoeff σ α)) (nhds 0) ≤ nhds 0
Tactic:
apply continuous_constantCoeff.continuousAt
Proof state after:
no goals
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : Filter.Tendsto (fun n => (constantCoeff σ α) (f ^ n)) Filter.atTop (nhds 0)
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
simp only [Filter.tendsto_def] at this
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
specialize this {0} _
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ {0} ∈ nhds 0

σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ {0} ∈ nhds 0

σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
suffices  ∀ x : α, {x} ∈ nhds x by exact this 0
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ ∀ (x : α), {x} ∈ nhds x

σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ ∀ (x : α), {x} ∈ nhds x

σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
rw [← discreteTopology_iff_singleton_mem_nhds]
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ DiscreteTopology α

σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ DiscreteTopology α

σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
infer_instance
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
simp only [map_pow, Filter.mem_atTop_sets, ge_iff_le, Set.mem_preimage,
  Set.mem_singleton_iff] at this
Proof state after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∃ a, ∀ (b : ℕ), a ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∃ a, ∀ (b : ℕ), a ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
obtain ⟨m, hm⟩ := this
Proof state after:
case intro
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ α) f)
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
case intro
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
use m
Proof state after:
case h
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ (constantCoeff σ α) f ^ m = 0
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
case h
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ (constantCoeff σ α) f ^ m = 0
Tactic:
apply hm m (le_refl m)
Proof state after:
no goals
Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff
Proof state before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this✝ : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
this : ∀ (x : α), {x} ∈ nhds x
⊢ {0} ∈ nhds 0
Tactic:
exact this 0
Proof state after:
no goals
Theorem: MvPowerSeries.hasSum_of_monomials_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
⊢ HasSum (fun d => (monomial α d) ((coeff α d) f)) f
Tactic:
rw [Pi.hasSum]
Proof state after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i => (monomial α i) ((coeff α i) f) x) (f x)
Theorem: MvPowerSeries.hasSum_of_monomials_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i => (monomial α i) ((coeff α i) f) x) (f x)
Tactic:
intro d
Proof state after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ HasSum (fun i => (monomial α i) ((coeff α i) f) d) (f d)
Theorem: MvPowerSeries.hasSum_of_monomials_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ HasSum (fun i => (monomial α i) ((coeff α i) f) d) (f d)
Tactic:
have hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0 := by
  intro d' h
  change coeff α d ((monomial α d') ((coeff α d') f)) = 0
  rw [coeff_monomial_ne (Ne.symm h)]
Proof state after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
⊢ HasSum (fun i => (monomial α i) ((coeff α i) f) d) (f d)
Theorem: MvPowerSeries.hasSum_of_monomials_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
⊢ HasSum (fun i => (monomial α i) ((coeff α i) f) d) (f d)
Tactic:
convert hasSum_single d hd using 1
Proof state after:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
⊢ f d = (monomial α d) ((coeff α d) f) d
Theorem: MvPowerSeries.hasSum_of_monomials_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
Tactic:
intro d' h
Proof state after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d d' : σ →₀ ℕ
h : d' ≠ d
⊢ (monomial α d') ((coeff α d') f) d = 0
Theorem: MvPowerSeries.hasSum_of_monomials_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d d' : σ →₀ ℕ
h : d' ≠ d
⊢ (monomial α d') ((coeff α d') f) d = 0
Tactic:
change coeff α d ((monomial α d') ((coeff α d') f)) = 0
Proof state after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d d' : σ →₀ ℕ
h : d' ≠ d
⊢ (coeff α d) ((monomial α d') ((coeff α d') f)) = 0
Theorem: MvPowerSeries.hasSum_of_monomials_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d d' : σ →₀ ℕ
h : d' ≠ d
⊢ (coeff α d) ((monomial α d') ((coeff α d') f)) = 0
Tactic:
rw [coeff_monomial_ne (Ne.symm h)]
Proof state after:
no goals
Theorem: MvPowerSeries.hasSum_of_monomials_self
Proof state before:
case h.e'_6
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : MvPowerSeries σ α
d : σ →₀ ℕ
hd : ∀ (d' : σ →₀ ℕ), d' ≠ d → (monomial α d') ((coeff α d') f) d = 0
⊢ f d = (monomial α d) ((coeff α d) f) d
Tactic:
rw [← coeff_apply f d, ← coeff_apply (monomial α d (coeff α d f)) d, coeff_apply,
  coeff_monomial_same]
Proof state after:
no goals
Theorem: MvPowerSeries.hasSum_of_homogeneous_components_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ HasSum (fun p => (homogeneousComponent w p) f) f
Tactic:
rw [Pi.hasSum]
Proof state after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i => (homogeneousComponent w i) f x) (f x)
Theorem: MvPowerSeries.hasSum_of_homogeneous_components_self
Proof state before:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ ∀ (x : σ →₀ ℕ), HasSum (fun i => (homogeneousComponent w i) f x) (f x)
Tactic:
intro d
Proof state after:
σ : Type u_2
α : Type u_1
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ HasSum (fun i => (homogeneousComponent w i) f d) (f d)