Theorem: MvPowerSeries.StronglySummable.coeff_sum (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
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
⊢ (coeff α d) hf.sum = ∑ i ∈ s, (coeff α d) (f i)
Tactic:
rw [coeff_sum_def, sum_subset (Finite.toFinset_subset.mpr hs)]
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
⊢ ∀ x ∈ s, x ∉ ⋯.toFinset → (coeff α d) (f x) = 0

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
⊢ ∀ x ∈ s, x ∉ ⋯.toFinset → (coeff α d) (f x) = 0
Tactic:
intro i _ hi'
State after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
i : ι
a✝ : i ∈ s
hi' : i ∉ ⋯.toFinset
⊢ (coeff α d) (f i) = 0

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
s : Finset ι
hs : (support fun i => (coeff α d) (f i)) ⊆ ↑s
i : ι
a✝ : i ∈ s
hi' : i ∉ ⋯.toFinset
⊢ (coeff α d) (f i) = 0
Tactic:
simpa only [Finite.mem_toFinset, Function.mem_support, Classical.not_not] using hi'
State after:
no goals