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

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => (coeff α d) (f i)) ((coeff α d) hf.sum)
Tactic:
apply hasSum_sum_of_ne_finset_zero
State after:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ ∀ b ∉ ⋯.toFinset, (coeff α d) (f b) = 0

State before:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ ∀ b ∉ ⋯.toFinset, (coeff α d) (f b) = 0
Tactic:
intro b hb
State after:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
b : ι
hb : b ∉ ⋯.toFinset
⊢ (coeff α d) (f b) = 0

State before:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
b : ι
hb : b ∉ ⋯.toFinset
⊢ (coeff α d) (f b) = 0
Tactic:
rw [Finite.mem_toFinset, Function.mem_support, Classical.not_not] at hb
State after:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
b : ι
hb : (coeff α d) (f b) = 0
⊢ (coeff α d) (f b) = 0

State before:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
b : ι
hb : (coeff α d) (f b) = 0
⊢ (coeff α d) (f b) = 0
Tactic:
exact hb
State after:
no goals