no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
h : HasDerivAt f f' x
hf' : f' ≠ 0
z : 𝕜
⊢ ‖z‖ ≤ ‖f'‖⁻¹ * ‖↑(ContinuousLinearMap.smulRight 1 f') z‖
field_simp [norm_smul, mt norm_eq_zero.1 hf']