no goals
𝕜 : Type u_3
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.474760
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.474855
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
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : ∀ (x : E), ↑f₀' x = ↑f₁' x
y : E
hy : f₀ y = f₁ y
⊢ (fun x' => f₀ x' - f₀ x - ↑f₀' (x' - x)) y = (fun x' => f₁ x' - f₁ x - ↑f₁' (x' - x)) y
simp only [hy, h₁, hx]