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

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
⊢ hf.sum = ⋯.sum + ⋯.sum
Tactic:
rw [← sum_add (hf.of_indicator s) (hf.of_indicator (sᶜ))]
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
⊢ hf.sum = ⋯.sum

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
⊢ hf.sum = ⋯.sum
Tactic:
exact sum_congr (s.indicator_self_add_compl f).symm
State after:
no goals