Theorem: MvPowerSeries.StronglySummable.add (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ StronglySummable (f + g)
Tactic:
classical exact fun d => Finite.subset (finite_toSet _) (support_add hf hg d)
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
⊢ StronglySummable (f + g)
Tactic:
exact fun d => Finite.subset (finite_toSet _) (support_add hf hg d)
State after:
no goals