refine @TendstoLocallyUniformlyOn.differentiableOn _ _ _ _ _ _ _ id f hf ?_ ?_ hU
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ f ∈ 𝓗 U
case refine_1
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ TendstoLocallyUniformlyOn id f (𝓝 f ⊓ 𝓟 (𝓗 U)) U

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