-- Mathlib/Topology/ContinuousMap/Compact.lean
theorem summable_of_locally_summable_norm {ι : Type*} {F : ι → C(X, E)}
    (hF : ∀ K : Compacts X, Summable fun i => ‖(F i).restrict K‖) : Summable F

Proof state:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ (restrict (↑K) (∑ i ∈ s, F i)) x = ∑ c ∈ s, (restrict (↑K) (F c)) x

Tactic:
erw [restrict_apply, restrict_apply, restrict_apply, restrict_apply]

Result:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ (∑ i ∈ s, F i) ↑x = ∑ c ∈ s, (restrict (↑K) (F c)) x

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
⊢ restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict (↑K) (F i)

Tactic:
ext1 x

Result:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ (restrict (↑K) (∑ i ∈ s, F i)) x = (∑ i ∈ s, restrict (↑K) (F i)) x

Proof state:
case intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
A : ∀ (s : Finset ι), restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict (↑K) (F i)
⊢ ∃ f, Filter.Tendsto (fun i => restrict (↑K) (∑ b ∈ i, F b)) Filter.atTop (nhds f)

Tactic:
simpa only [HasSum, A] using (hF K).of_norm

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
⊢ Summable F

Tactic:
refine (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => ?_

Result:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Set X
hK : IsCompact K
⊢ ∃ f, Filter.Tendsto (fun i => restrict K (∑ b ∈ i, F b)) Filter.atTop (nhds f)

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∀ (s : Finset ι), restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict (↑K) (F i)

Tactic:
intro s

Result:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
⊢ restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict (↑K) (F i)

Proof state:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ (∑ i ∈ s, F i) ↑x = ∑ c ∈ s, (restrict (↑K) (F c)) x

Tactic:
simp only [coe_sum, Finset.sum_apply]

Result:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ ∑ c ∈ s, (F c) ↑x = ∑ c ∈ s, (restrict (↑K) (F c)) x

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
⊢ Summable F

Tactic:
classical
refine (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => ?_
lift K to Compacts X using hK
have A : ∀ s : Finset ι, restrict (↑K) (∑ i ∈ s, F i) = ∑ i ∈ s, restrict K (F i) := by
  intro s
  ext1 x
  simp
  erw [restrict_apply, restrict_apply, restrict_apply, restrict_apply]
  simp? says simp only [coe_sum, Finset.sum_apply]
  congr!
simpa only [HasSum, A] using (hF K).of_norm

Result:
no goals

Proof state:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ ∑ c ∈ s, (F c) ↑x = ∑ c ∈ s, (restrict (↑K) (F c)) x

Tactic:
congr!

Result:
no goals

Proof state:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ (restrict (↑K) (∑ i ∈ s, F i)) x = (∑ i ∈ s, restrict (↑K) (F i)) x

Tactic:
simp

Result:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ (restrict (↑K) (∑ i ∈ s, F i)) x = ∑ c ∈ s, (restrict (↑K) (F c)) x

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Set X
hK : IsCompact K
⊢ ∃ f, Filter.Tendsto (fun i => restrict K (∑ b ∈ i, F b)) Filter.atTop (nhds f)

Tactic:
lift K to Compacts X using hK

Result:
case intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
⊢ ∃ f, Filter.Tendsto (fun i => restrict (↑K) (∑ b ∈ i, F b)) Filter.atTop (nhds f)

Proof state:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ (∑ i ∈ s, F i) ↑x = ∑ c ∈ s, (restrict (↑K) (F c)) x

Tactic:
simp? says simp only [coe_sum, Finset.sum_apply]

Result:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i => ‖restrict (↑K) (F i)‖
K : Compacts X
s : Finset ι
x : ↑↑K
⊢ ∑ c ∈ s, (F c) ↑x = ∑ c ∈ s, (restrict (↑K) (F c)) x