-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/-- The negative logarithmtic derivative of `s ↦ (s - 1) * L χ s` for a trivial
Dirichlet character `χ` is continuous away from the zeros of `L χ` (including at `s = 1`). -/
lemma continuousOn_neg_logDeriv_LFunctionTrivChar₁ :
    ContinuousOn (fun s ↦ -deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s)
      {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Proof state:
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
⊢ LFunctionTrivChar₁ n w ≠ 0

Tactic:
rcases eq_or_ne w 1 with rfl | hw'

Result:
case inl
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
hw : 1 ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
⊢ LFunctionTrivChar₁ n 1 ≠ 0

case inr
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
hw' : w ≠ 1
⊢ LFunctionTrivChar₁ n w ≠ 0

Proof state:
case inl
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
hw : 1 ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
⊢ LFunctionTrivChar₁ n 1 ≠ 0

Tactic:
exact LFunctionTrivChar₁_apply_one_ne_zero _

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
⊢ ContinuousOn (fun s => -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
refine ((h.contDiff.continuous_deriv le_rfl).continuousOn.div
  h.continuous.continuousOn fun w hw ↦ ?_).neg

Result:
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
⊢ LFunctionTrivChar₁ n w ≠ 0

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ ContinuousOn (fun s => -deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s)
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
simp_rw [neg_div]

Result:
n : ℕ
inst✝ : NeZero n
⊢ ContinuousOn (fun s => -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Proof state:
case inr
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
hw' : w ≠ 1
⊢ LFunctionTrivChar₁ n w ≠ 0

Tactic:
rw [LFunctionTrivChar₁, Function.update_of_ne hw', mul_ne_zero_iff]

Result:
case inr
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
hw' : w ≠ 1
⊢ w - 1 ≠ 0 ∧ LFunctionTrivChar n w ≠ 0

Proof state:
case inr
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
hw' : w ≠ 1
⊢ w - 1 ≠ 0 ∧ LFunctionTrivChar n w ≠ 0

Tactic:
exact ⟨sub_ne_zero_of_ne hw', (Set.mem_setOf.mp hw).resolve_left hw'⟩

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ ContinuousOn (fun s => -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
have h := differentiable_LFunctionTrivChar₁ n

Result:
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
⊢ ContinuousOn (fun s => -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}