Theorem: MvPowerSeries.as_tsum_of_homogeneous_components_self (DividedPowers/ForMathlib/MvPowerSeries/Topology.lean)

State before:
σ : Type u_2
α : Type u_1
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f = ∑' (p : ℕ), (homogeneousComponent w p) f
Tactic:
haveI := t2Space σ α
State after:
σ : Type u_2
α : Type u_1
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
w : σ → ℕ
f : MvPowerSeries σ α
this : T2Space (MvPowerSeries σ α)
⊢ f = ∑' (p : ℕ), (homogeneousComponent w p) f

State before:
σ : Type u_2
α : Type u_1
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
w : σ → ℕ
f : MvPowerSeries σ α
this : T2Space (MvPowerSeries σ α)
⊢ f = ∑' (p : ℕ), (homogeneousComponent w p) f
Tactic:
exact HasSum.unique (hasSum_of_homogeneous_components_self w f)
 (homogeneous_components_self_summable w f).hasSum
State after:
no goals