Theorem: deriv.ofReal_comp (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
by_cases hf : DifferentiableAt ℝ f z
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
exact hf.hasDerivAt.ofReal_comp.deriv
State after:
no goals

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
have hf' := mt DifferentiableAt.ofReal_comp_iff.mp hf
State after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
hf' : ¬DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
hf' : ¬DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
Tactic:
rw [deriv_zero_of_not_differentiableAt hf, deriv_zero_of_not_differentiableAt <| hf',
  Complex.ofReal_zero]
State after:
no goals