Theorem: DifferentiableAt.ofReal_comp_iff (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
⊢ DifferentiableAt ℝ (fun y => ↑(f y)) z ↔ DifferentiableAt ℝ f z
Tactic:
refine ⟨fun H ↦ ?_, ofReal_comp⟩
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ DifferentiableAt ℝ f z

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ DifferentiableAt ℝ f z
Tactic:
obtain ⟨u, _, hu₂⟩ := H.hasDerivAt.of_hasDerivAt_ofReal_comp
State after:
case intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
u : ℝ
left✝ : deriv (fun y => ↑(f y)) z = ↑u
hu₂ : HasDerivAt (fun y => f y) u z
⊢ DifferentiableAt ℝ f z

State before:
case intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
H : DifferentiableAt ℝ (fun y => ↑(f y)) z
u : ℝ
left✝ : deriv (fun y => ↑(f y)) z = ↑u
hu₂ : HasDerivAt (fun y => f y) u z
⊢ DifferentiableAt ℝ f z
Tactic:
exact HasDerivAt.differentiableAt hu₂
State after:
no goals