simp [eventually_inf_principal, 𝓗]
case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (n : ℂ → ℂ) in 𝓝 f ⊓ 𝓟 (𝓗 U), DifferentiableOn ℂ (id n) U
case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (x : ℂ → ℂ) in 𝓝 f, x ∈ {f | DifferentiableOn ℂ f U} → DifferentiableOn ℂ x U