Theorem: deriv_fun_re (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
⊢ (deriv fun {σ₂} => f (↑σ₂ + ↑t * I)) = fun σ => deriv f (↑σ + ↑t * I)
Tactic:
ext σ
State after:
case h
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)

State before:
case h
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)
Tactic:
have := deriv.comp (h := fun (σ : ℝ) ↦ σ + t * I) (h₂ := f) σ (diff σ) ?_
State after:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f ((fun σ => ↑σ + ↑t * I) σ) * deriv (fun σ => ↑σ + ↑t * I) σ
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)

case h.refine_1
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ DifferentiableAt ℝ (fun σ => ↑σ + ↑t * I) σ

State before:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f ((fun σ => ↑σ + ↑t * I) σ) * deriv (fun σ => ↑σ + ↑t * I) σ
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)
Tactic:
simp only [deriv_add_const', _root_.deriv_ofReal, mul_one] at this
State after:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f (↑σ + ↑t * I)
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)

State before:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f (↑σ + ↑t * I)
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)
Tactic:
rw [← this]
State after:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f (↑σ + ↑t * I)
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv (f ∘ fun σ => ↑σ + ↑t * I) σ

State before:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f (↑σ + ↑t * I)
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv (f ∘ fun σ => ↑σ + ↑t * I) σ
Tactic:
rfl
State after:
no goals

State before:
case h.refine_1
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ DifferentiableAt ℝ (fun σ => ↑σ + ↑t * I) σ
Tactic:
apply DifferentiableAt.add_const <| differentiableAt_ofReal σ
State after:
no goals