𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.296313
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.296408
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
ι : Type u_1
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ (i : ι), i ∈ u → (fun p => A i p.fst - A i p.snd - ↑(A' i) (p.fst - p.snd)) =o[𝓝 (x, x)] fun p => p.fst - p.snd
⊢ (fun p => ∑ i in u, A i p.fst - ∑ i in u, A i p.snd - ↑(∑ i in u, A' i) (p.fst - p.snd)) =o[𝓝 (x, x)] fun p =>
    p.fst - p.snd
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.296313
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.296408
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
ι : Type u_1
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ (i : ι), i ∈ u → HasStrictFDerivAt (A i) (A' i) x
⊢ HasStrictFDerivAt (fun y => ∑ i in u, A i y) (∑ i in u, A' i) x
dsimp [HasStrictFDerivAt] at *
case h.e'_7.h
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.296313
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.296408
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
ι : Type u_1
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ (i : ι), i ∈ u → (fun p => A i p.fst - A i p.snd - ↑(A' i) (p.fst - p.snd)) =o[𝓝 (x, x)] fun p => p.fst - p.snd
x✝ : E × E
⊢ ∑ i in u, A i x✝.fst - ∑ i in u, A i x✝.snd - ↑(∑ i in u, A' i) (x✝.fst - x✝.snd) =
    ∑ i in u, (A i x✝.fst - A i x✝.snd - ↑(A' i) (x✝.fst - x✝.snd))
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.296313
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.296408
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
ι : Type u_1
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ (i : ι), i ∈ u → (fun p => A i p.fst - A i p.snd - ↑(A' i) (p.fst - p.snd)) =o[𝓝 (x, x)] fun p => p.fst - p.snd
⊢ (fun p => ∑ i in u, A i p.fst - ∑ i in u, A i p.snd - ↑(∑ i in u, A' i) (p.fst - p.snd)) =o[𝓝 (x, x)] fun p =>
    p.fst - p.snd
convert IsLittleO.sum h
no goals
case h.e'_7.h
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.296313
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.296408
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
ι : Type u_1
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ (i : ι), i ∈ u → (fun p => A i p.fst - A i p.snd - ↑(A' i) (p.fst - p.snd)) =o[𝓝 (x, x)] fun p => p.fst - p.snd
x✝ : E × E
⊢ ∑ i in u, A i x✝.fst - ∑ i in u, A i x✝.snd - ↑(∑ i in u, A' i) (x✝.fst - x✝.snd) =
    ∑ i in u, (A i x✝.fst - A i x✝.snd - ↑(A' i) (x✝.fst - x✝.snd))
simp [Finset.sum_sub_distrib, ContinuousLinearMap.sum_apply]