Adapted from PrimeNumberTheoremAnd revision 127b50e33f6033e2147921167a117af96d9ba4ea, via Jason Davies's Iwaniec linear sieve snapshot c8d01549d2ae640b36ec198c1f0f6495f1b036cf (both Apache-2.0). Blueprint-only machinery is omitted.

Auxiliary lemmas

theorem Complex.hasDerivAt_ofReal (x : ℝ) : HasDerivAt ofReal 1 x

theorem Complex.deriv_ofReal (x : ℝ) : deriv ofReal x = 1

theorem Complex.differentiableAt_ofReal (x : ℝ) : DifferentiableAt ℝ ofReal x

theorem DifferentiableAt.comp_ofReal {e : ℂ → ℂ} {z : ℝ} (hf : DifferentiableAt ℂ e ↑z) : DifferentiableAt ℝ (fun (x : ℝ) => e ↑x) z

theorem deriv.comp_ofReal {e : ℂ → ℂ} {z : ℝ} (hf : DifferentiableAt ℂ e ↑z) : deriv (fun (x : ℝ) => e ↑x) z = deriv e ↑z

theorem Differentiable.comp_ofReal {e : ℂ → ℂ} (h : Differentiable ℂ e) : Differentiable ℝ fun (x : ℝ) => e ↑x

theorem DifferentiableAt.ofReal_comp {z : ℝ} {f : ℝ → ℝ} (hf : DifferentiableAt ℝ f z) : DifferentiableAt ℝ (fun (y : ℝ) => ↑(f y)) z

theorem Differentiable.ofReal_comp {f : ℝ → ℝ} (hf : Differentiable ℝ f) : Differentiable ℝ fun (y : ℝ) => ↑(f y)

theorem HasDerivAt.of_hasDerivAt_ofReal_comp {z : ℝ} {f : ℝ → ℝ} {u : ℂ} (hf : HasDerivAt (fun (y : ℝ) => ↑(f y)) u z) : ∃ (u' : ℝ), u = ↑u' ∧ HasDerivAt f u' z

theorem DifferentiableAt.ofReal_comp_iff {z : ℝ} {f : ℝ → ℝ} : DifferentiableAt ℝ (fun (y : ℝ) => ↑(f y)) z ↔ DifferentiableAt ℝ f z

theorem Differentiable.ofReal_comp_iff {f : ℝ → ℝ} : (Differentiable ℝ fun (y : ℝ) => ↑(f y)) ↔ Differentiable ℝ f

theorem deriv.ofReal_comp {z : ℝ} {f : ℝ → ℝ} : deriv (fun (y : ℝ) => ↑(f y)) z = ↑(deriv f z)