Theorem: deriv_ζ₁_apply_of_ne_one (EulerProducts/PNT.lean)

State before:
z : ℂ
hz : z ≠ 1
⊢ deriv ζ₁ z = deriv ζ z * (z - 1) + ζ z
Tactic:
have H : deriv ζ₁ z = deriv (fun w ↦ ζ w * (w - 1)) z := by
  refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_
  refine ⟨{w | w ≠ 1}, IsOpen.mem_nhds isOpen_ne hz, fun w hw ↦ ?_⟩
  simp only [ζ₁, ne_eq, Set.mem_setOf.mp hw, not_false_eq_true, Function.update_noteq]
State after:
z : ℂ
hz : z ≠ 1
H : deriv ζ₁ z = deriv (fun w => ζ w * (w - 1)) z
⊢ deriv ζ₁ z = deriv ζ z * (z - 1) + ζ z

State before:
z : ℂ
hz : z ≠ 1
H : deriv ζ₁ z = deriv (fun w => ζ w * (w - 1)) z
⊢ deriv ζ₁ z = deriv ζ z * (z - 1) + ζ z
Tactic:
rw [H, deriv_mul (differentiableAt_riemannZeta hz) <| differentiableAt_id'.sub <|
  differentiableAt_const 1, deriv_sub_const, deriv_id'', mul_one]
State after:
no goals

State before:
z : ℂ
hz : z ≠ 1
⊢ deriv ζ₁ z = deriv (fun w => ζ w * (w - 1)) z
Tactic:
refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_
State after:
z : ℂ
hz : z ≠ 1
⊢ ∃ s ∈ nhds z, Set.EqOn ζ₁ (fun w => ζ w * (w - 1)) s

State before:
z : ℂ
hz : z ≠ 1
⊢ ∃ s ∈ nhds z, Set.EqOn ζ₁ (fun w => ζ w * (w - 1)) s
Tactic:
refine ⟨{w | w ≠ 1}, IsOpen.mem_nhds isOpen_ne hz, fun w hw ↦ ?_⟩
State after:
z : ℂ
hz : z ≠ 1
w : ℂ
hw : w ∈ {w | w ≠ 1}
⊢ ζ₁ w = (fun w => ζ w * (w - 1)) w

State before:
z : ℂ
hz : z ≠ 1
w : ℂ
hw : w ∈ {w | w ≠ 1}
⊢ ζ₁ w = (fun w => ζ w * (w - 1)) w
Tactic:
simp only [ζ₁, ne_eq, Set.mem_setOf.mp hw, not_false_eq_true, Function.update_noteq]
State after:
no goals