feat(analysis/calculus/{f,}deriv): add some iff lemmas (#11363)

src/analysis/calculus/deriv.lean

@@ -377,6 +377,13 @@ h.has_fderiv_within_at.has_deriv_within_at
 lemma differentiable_at.has_deriv_at (h : differentiable_at 𝕜 f x) : has_deriv_at f (deriv f x) x :=
 h.has_fderiv_at.has_deriv_at
 
+@[simp] lemma has_deriv_at_deriv_iff : has_deriv_at f (deriv f x) x ↔ differentiable_at 𝕜 f x :=
+⟨λ h, h.differentiable_at, λ h, h.has_deriv_at⟩
+
+@[simp] lemma has_deriv_within_at_deriv_within_iff :
+  has_deriv_within_at f (deriv_within f s x) s x ↔ differentiable_within_at 𝕜 f s x :=
+⟨λ h, h.differentiable_within_at, λ h, h.has_deriv_within_at⟩
+
 lemma differentiable_on.has_deriv_at (h : differentiable_on 𝕜 f s) (hs : s ∈ 𝓝 x) :
   has_deriv_at f (deriv f x) x :=
 (h.has_fderiv_at hs).has_deriv_at

src/analysis/calculus/fderiv.lean

@@ -685,6 +685,32 @@ lemma has_fderiv_at_filter.congr_of_eventually_eq (h : has_fderiv_at_filter f f'
   (hL : f₁ =ᶠ[L] f) (hx : f₁ x = f x) : has_fderiv_at_filter f₁ f' x L :=
 (hL.has_fderiv_at_filter_iff hx $ λ _, rfl).2 h
 
+theorem filter.eventually_eq.has_fderiv_at_iff (h : f₀ =ᶠ[𝓝 x] f₁) :
+  has_fderiv_at f₀ f' x ↔ has_fderiv_at f₁ f' x :=
+h.has_fderiv_at_filter_iff h.eq_of_nhds (λ _, rfl)
+
+theorem filter.eventually_eq.differentiable_at_iff (h : f₀ =ᶠ[𝓝 x] f₁) :
+  differentiable_at 𝕜 f₀ x ↔ differentiable_at 𝕜 f₁ x :=
+exists_congr $ λ f', h.has_fderiv_at_iff
+
+theorem filter.eventually_eq.has_fderiv_within_at_iff (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : f₀ x = f₁ x) :
+  has_fderiv_within_at f₀ f' s x ↔ has_fderiv_within_at f₁ f' s x :=
+h.has_fderiv_at_filter_iff hx (λ _, rfl)
+
+theorem filter.eventually_eq.has_fderiv_within_at_iff_of_mem (h : f₀ =ᶠ[𝓝[s] x] f₁) (hx : x ∈ s) :
+  has_fderiv_within_at f₀ f' s x ↔ has_fderiv_within_at f₁ f' s x :=
+h.has_fderiv_within_at_iff (h.eq_of_nhds_within hx)
+
+theorem filter.eventually_eq.differentiable_within_at_iff (h : f₀ =ᶠ[𝓝[s] x] f₁)
+  (hx : f₀ x = f₁ x) :
+  differentiable_within_at 𝕜 f₀ s x ↔ differentiable_within_at 𝕜 f₁ s x :=
+exists_congr $ λ f', h.has_fderiv_within_at_iff hx
+
+theorem filter.eventually_eq.differentiable_within_at_iff_of_mem (h : f₀ =ᶠ[𝓝[s] x] f₁)
+  (hx : x ∈ s) :
+  differentiable_within_at 𝕜 f₀ s x ↔ differentiable_within_at 𝕜 f₁ s x :=
+h.differentiable_within_at_iff (h.eq_of_nhds_within hx)
+
 lemma has_fderiv_within_at.congr_mono (h : has_fderiv_within_at f f' s x) (ht : ∀x ∈ t, f₁ x = f x)
   (hx : f₁ x = f x) (h₁ : t ⊆ s) : has_fderiv_within_at f₁ f' t x :=
 has_fderiv_at_filter.congr_of_eventually_eq (h.mono h₁) (filter.mem_inf_of_right ht) hx
@@ -733,8 +759,7 @@ lemma differentiable_on_congr (h' : ∀x ∈ s, f₁ x = f x) :
 
 lemma differentiable_at.congr_of_eventually_eq (h : differentiable_at 𝕜 f x) (hL : f₁ =ᶠ[𝓝 x] f) :
   differentiable_at 𝕜 f₁ x :=
-has_fderiv_at.differentiable_at
-  (has_fderiv_at_filter.congr_of_eventually_eq h.has_fderiv_at hL (mem_of_mem_nhds hL : _))
+hL.differentiable_at_iff.2 h
 
 lemma differentiable_within_at.fderiv_within_congr_mono (h : differentiable_within_at 𝕜 f s x)
   (hs : ∀x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (hxt : unique_diff_within_at 𝕜 t x) (h₁ : t ⊆ s) :