Theorem: LinearDerivative_ofReal (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
x : ℝ
a b : ℂ
⊢ HasDerivAt (fun t => a * ↑t + b) a x
Tactic:
refine HasDerivAt.add_const ?_ b
State after:
x : ℝ
a b : ℂ
⊢ HasDerivAt (fun t => a * ↑t) a x

State before:
x : ℝ
a b : ℂ
⊢ HasDerivAt (fun t => a * ↑t) a x
Tactic:
convert (ContinuousLinearMap.hasDerivAt Complex.ofRealCLM).const_mul a using 1
State after:
case h.e'_7
x : ℝ
a b : ℂ
⊢ a = a * ofRealCLM 1

State before:
case h.e'_7
x : ℝ
a b : ℂ
⊢ a = a * ofRealCLM 1
Tactic:
simp
State after:
no goals