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 𝕜
f : 𝕜 → F
s : Set F
x : 𝕜
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
by_cases hx : DifferentiableAt 𝕜 f x <;> simp [deriv_zero_of_not_differentiableAt, *]