Theorem: HasDerivAt.of_hasDerivAt_ofReal_comp (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
⊢ ∃ u', u = ↑u' ∧ HasDerivAt f u' z
Tactic:
lift u to ℝ
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
⊢ u.im = 0

case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ ∃ u', ↑u = ↑u' ∧ HasDerivAt f u' z

State before:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ ∃ u', ↑u = ↑u' ∧ HasDerivAt f u' z
Tactic:
refine ⟨u, rfl, ?_⟩
State after:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ HasDerivAt f u z

State before:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ HasDerivAt f u z
Tactic:
convert (reCLM.hasFDerivAt.comp z hf.hasFDerivAt).hasDerivAt
State after:
case h.e'_7
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ u = (reCLM.comp (smulRight 1 ↑u)) 1

State before:
case h.e'_7
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ u = (reCLM.comp (smulRight 1 ↑u)) 1
Tactic:
rw [comp_apply, smulRight_apply, one_apply, one_smul, reCLM_apply, ofReal_re]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
⊢ u.im = 0
Tactic:
have H := (imCLM.hasFDerivAt.comp z hf.hasFDerivAt).hasDerivAt.deriv
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : _root_.deriv (⇑imCLM ∘ fun y => ↑(f y)) z = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : _root_.deriv (⇑imCLM ∘ fun y => ↑(f y)) z = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Tactic:
simp only [Function.comp_def, imCLM_apply, ofReal_im, deriv_const] at H
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : 0 = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : 0 = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
Tactic:
rwa [eq_comm, comp_apply, imCLM_apply, smulRight_apply, one_apply, one_smul] at H
State after:
no goals