`BookProof.LimitCircleExample.hasDerivAt_lcLogFun` (x : ℝ) : HasDerivAt (fun y : ℝ => ((lcP y : ℝ) : ℂ) + Complex.I * ((lcQ y : ℝ) : ℂ)) (lcLog' x) x

Initializing...

`BookProof.LimitCircleExample.hasDerivAt_lcLogFun` (x : ℝ) : HasDerivAt (fun y : ℝ => ((lcP y : ℝ) : ℂ) + Complex.I * ((lcQ y : ℝ) : ℂ)) (lcLog' x) x · Prove2Me