Theorem: ζ₁_differentiable (EulerProducts/PNT.lean)

State before:
⊢ Differentiable ℂ ζ₁
Tactic:
rw [← differentiableOn_univ,
  ← differentiableOn_compl_singleton_and_continuousAt_iff (c := 1) Filter.univ_mem, ζ₁]
State after:
⊢ DifferentiableOn ℂ (Function.update (fun z => ζ z * (z - 1)) 1 1) (Set.univ \ {1}) ∧
    ContinuousAt (Function.update (fun z => ζ z * (z - 1)) 1 1) 1

State before:
⊢ DifferentiableOn ℂ (Function.update (fun z => ζ z * (z - 1)) 1 1) (Set.univ \ {1}) ∧
    ContinuousAt (Function.update (fun z => ζ z * (z - 1)) 1 1) 1
Tactic:
refine ⟨DifferentiableOn.congr (f := fun z ↦ ζ z * (z - 1))
  (fun _ hz ↦ DifferentiableAt.differentiableWithinAt ?_) fun _ hz ↦ ?_,
  continuousWithinAt_compl_self.mp ?_⟩
State after:
case refine_1
x✝ : ℂ
hz : x✝ ∈ Set.univ \ {1}
⊢ DifferentiableAt ℂ (fun z => ζ z * (z - 1)) x✝

case refine_2
x✝ : ℂ
hz : x✝ ∈ Set.univ \ {1}
⊢ Function.update (fun z => ζ z * (z - 1)) 1 1 x✝ = (fun z => ζ z * (z - 1)) x✝

case refine_3

⊢ ContinuousWithinAt (Function.update (fun z => ζ z * (z - 1)) 1 1) {1}ᶜ 1

State before:
case refine_1
x✝ : ℂ
hz : x✝ ∈ Set.univ \ {1}
⊢ DifferentiableAt ℂ (fun z => ζ z * (z - 1)) x✝
Tactic:
simp only [Set.mem_diff, Set.mem_univ, Set.mem_singleton_iff, true_and] at hz
State after:
case refine_1
x✝ : ℂ
hz : ¬x✝ = 1
⊢ DifferentiableAt ℂ (fun z => ζ z * (z - 1)) x✝

State before:
case refine_1
x✝ : ℂ
hz : ¬x✝ = 1
⊢ DifferentiableAt ℂ (fun z => ζ z * (z - 1)) x✝
Tactic:
exact (differentiableAt_riemannZeta hz).mul <| (differentiableAt_id').sub <|
  differentiableAt_const 1
State after:
no goals

State before:
case refine_2
x✝ : ℂ
hz : x✝ ∈ Set.univ \ {1}
⊢ Function.update (fun z => ζ z * (z - 1)) 1 1 x✝ = (fun z => ζ z * (z - 1)) x✝
Tactic:
simp only [Set.mem_diff, Set.mem_univ, Set.mem_singleton_iff, true_and] at hz
State after:
case refine_2
x✝ : ℂ
hz : ¬x✝ = 1
⊢ Function.update (fun z => ζ z * (z - 1)) 1 1 x✝ = (fun z => ζ z * (z - 1)) x✝

State before:
case refine_2
x✝ : ℂ
hz : ¬x✝ = 1
⊢ Function.update (fun z => ζ z * (z - 1)) 1 1 x✝ = (fun z => ζ z * (z - 1)) x✝
Tactic:
simp only [ne_eq, hz, not_false_eq_true, Function.update_noteq]
State after:
no goals

State before:
case refine_3

⊢ ContinuousWithinAt (Function.update (fun z => ζ z * (z - 1)) 1 1) {1}ᶜ 1
Tactic:
conv in (_ * _) => rw [mul_comm]
State after:
case refine_3

⊢ ContinuousWithinAt (Function.update (fun z => (z - 1) * ζ z) 1 1) {1}ᶜ 1

State before:
case refine_3

⊢ ContinuousWithinAt (Function.update (fun z => (z - 1) * ζ z) 1 1) {1}ᶜ 1
Tactic:
simp only [continuousWithinAt_compl_self, continuousAt_update_same]
State after:
case refine_3

⊢ Filter.Tendsto (fun z => (z - 1) * ζ z) (nhdsWithin 1 {1}ᶜ) (nhds 1)

State before:
case refine_3

⊢ Filter.Tendsto (fun z => (z - 1) * ζ z) (nhdsWithin 1 {1}ᶜ) (nhds 1)
Tactic:
exact riemannZeta_residue_one
State after:
no goals