𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.127337
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.127432
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
hf : HasFDerivAtFilter f f' x L
hg : HasFDerivAtFilter g g' x L
x✝ : E
⊢ f x✝ - f x - (↑f' x✝ - ↑f' x) + (g x✝ - g x - (↑g' x✝ - ↑g' x)) =
    f x✝ + g x✝ - (f x + g x) - (↑f' x✝ + ↑g' x✝ - (↑f' x + ↑g' x))
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.127337
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.127432
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
hf : HasFDerivAtFilter f f' x L
hg : HasFDerivAtFilter g g' x L
x✝ : E
⊢ f x✝ - f x - ↑f' (x✝ - x) + (g x✝ - g x - ↑g' (x✝ - x)) =
    (fun y => f y + g y) x✝ - (fun y => f y + g y) x - ↑(f' + g') (x✝ - x)
simp only [LinearMap.sub_apply, LinearMap.add_apply, map_sub, map_add, add_apply]
no goals
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.127337
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.127432
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
hf : HasFDerivAtFilter f f' x L
hg : HasFDerivAtFilter g g' x L
x✝ : E
⊢ f x✝ - f x - (↑f' x✝ - ↑f' x) + (g x✝ - g x - (↑g' x✝ - ↑g' x)) =
    f x✝ + g x✝ - (f x + g x) - (↑f' x✝ + ↑g' x✝ - (↑f' x + ↑g' x))
abel