Theorem: MvPowerSeries.StronglySummable.iff_summable' (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Topology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
⊢ StronglySummable f ↔ Filter.Tendsto f Filter.cofinite (nhds 0)
Tactic:
haveI := topologicalRing σ α
State after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ StronglySummable f ↔ Filter.Tendsto f Filter.cofinite (nhds 0)

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ StronglySummable f ↔ Filter.Tendsto f Filter.cofinite (nhds 0)
Tactic:
refine' ⟨fun hf => hf.summable.tendsto_cofinite_zero, _⟩
State after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ Filter.Tendsto f Filter.cofinite (nhds 0) → StronglySummable f

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ Filter.Tendsto f Filter.cofinite (nhds 0) → StronglySummable f
Tactic:
rw [StronglySummable, nhds_pi, Filter.tendsto_pi]
State after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ (∀ (i : σ →₀ ℕ), Filter.Tendsto (fun x => f x i) Filter.cofinite (nhds (0 i))) →
    ∀ (d : σ →₀ ℕ), (support fun i => (coeff α d) (f i)).Finite

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ (∀ (i : σ →₀ ℕ), Filter.Tendsto (fun x => f x i) Filter.cofinite (nhds (0 i))) →
    ∀ (d : σ →₀ ℕ), (support fun i => (coeff α d) (f i)).Finite
Tactic:
exact forall_imp fun d => finite_support_of_tendsto_zero
State after:
no goals