no goals
𝕜 : Type u
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type uX
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x x₀ : E
c : F
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
⊢ ContDiffAt 𝕜 1 f x ↔ ∃ f' u, u ∈ 𝓝 x ∧ ContinuousOn f' u ∧ ∀ (x : E), x ∈ u → HasFDerivAt f (f' x) x
simp_rw [show (1 : ℕ∞) = (0 + 1 : ℕ) from (zero_add 1).symm, contDiffAt_succ_iff_hasFDerivAt,
  show ((0 : ℕ) : ℕ∞) = 0 from rfl, contDiffAt_zero,
  exists_mem_and_iff antitone_bforall antitone_continuousOn, and_comm]