Theorem: MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto (DividedPowers/ForMathlib/MvPowerSeries/Topology.lean)

State before:
σ : Type u_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Semiring α
ι : Type u_2
f : ι → MvPowerSeries σ α
u : Filter ι
g : MvPowerSeries σ α
⊢ Filter.Tendsto f u (nhds g) ↔ ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Tactic:
rw [nhds_pi, Filter.tendsto_pi]
State after:
σ : Type u_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Semiring α
ι : Type u_2
f : ι → MvPowerSeries σ α
u : Filter ι
g : MvPowerSeries σ α
⊢ (∀ (i : σ →₀ ℕ), Filter.Tendsto (fun x => f x i) u (nhds (g i))) ↔
    ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))

State before:
σ : Type u_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Semiring α
ι : Type u_2
f : ι → MvPowerSeries σ α
u : Filter ι
g : MvPowerSeries σ α
⊢ (∀ (i : σ →₀ ℕ), Filter.Tendsto (fun x => f x i) u (nhds (g i))) ↔
    ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Tactic:
exact forall_congr' (fun d => Iff.rfl)
State after:
no goals