Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Topology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ hf.sum = tsum f
Tactic:
ext d
State after:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) (tsum f)

State before:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) (tsum f)
Tactic:
rw [tsum_def, dif_pos hf.summable]
State after:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) (if (support f).Finite then finsum f else Exists.choose ⋯)

State before:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) (if (support f).Finite then finsum f else Exists.choose ⋯)
Tactic:
apply HasSum.unique (hf.hasSum_coeff d)
State after:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => (coeff α d) (f i)) ((coeff α d) (if (support f).Finite then finsum f else Exists.choose ⋯))

State before:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => (coeff α d) (f i)) ((coeff α d) (if (support f).Finite then finsum f else Exists.choose ⋯))
Tactic:
apply HasSum.map
State after:
case h.hf
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => f i) (if (support f).Finite then finsum f else Exists.choose ⋯)

case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)

State before:
case h.hf
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => f i) (if (support f).Finite then finsum f else Exists.choose ⋯)

case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)
Tactic:
. split_ifs with h
  . rw [← tsum_eq_finsum h]
    exact hf.summable.hasSum
  . exact (Classical.choose_spec hf.summable)
State after:
case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)

State before:
case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)
Tactic:
. exact continuous_component σ α d
State after:
no goals

State before:
case h.hf
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => f i) (if (support f).Finite then finsum f else Exists.choose ⋯)
Tactic:
split_ifs with h
State after:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (finsum f)

case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (finsum f)

case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)
Tactic:
. rw [← tsum_eq_finsum h]
  exact hf.summable.hasSum
State after:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)

State before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)
Tactic:
. exact (Classical.choose_spec hf.summable)
State after:
no goals

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (finsum f)
Tactic:
rw [← tsum_eq_finsum h]
State after:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (∑' (b : ι), f b)

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (∑' (b : ι), f b)
Tactic:
exact hf.summable.hasSum
State after:
no goals

State before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)
Tactic:
exact (Classical.choose_spec hf.summable)
State after:
no goals

State before:
case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)
Tactic:
exact continuous_component σ α d
State after:
no goals