Theorem: Section17sheet2.Complex.differentiableAt_coe (FormalisingMathematics2024/Section17curvesAndSurfaces/Sheet2.lean)

State before:
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (fun y => ↑(f y)) x
Tactic:
apply Complex.ofRealClm.differentiableAt.comp _ hf
State after:
no goals