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

State before:
⊢ ContinuousOn (fun z => -deriv ζ₁ z / ζ₁ z) {z | z = 1 ∨ ζ z ≠ 0}
Tactic:
simp_rw [neg_div]
State after:
⊢ ContinuousOn (fun z => -(deriv ζ₁ z / ζ₁ z)) {z | z = 1 ∨ ζ z ≠ 0}

State before:
⊢ ContinuousOn (fun z => -(deriv ζ₁ z / ζ₁ z)) {z | z = 1 ∨ ζ z ≠ 0}
Tactic:
refine ((ζ₁_differentiable.contDiff.continuous_deriv le_rfl).continuousOn.div
  ζ₁_differentiable.continuous.continuousOn fun w hw ↦ ?_).neg
State after:
w : ℂ
hw : w ∈ {z | z = 1 ∨ ζ z ≠ 0}
⊢ ζ₁ w ≠ 0

State before:
w : ℂ
hw : w ∈ {z | z = 1 ∨ ζ z ≠ 0}
⊢ ζ₁ w ≠ 0
Tactic:
rcases eq_or_ne w 1 with rfl | hw'
State after:
case inl
hw : 1 ∈ {z | z = 1 ∨ ζ z ≠ 0}
⊢ ζ₁ 1 ≠ 0

case inr
w : ℂ
hw : w ∈ {z | z = 1 ∨ ζ z ≠ 0}
hw' : w ≠ 1
⊢ ζ₁ w ≠ 0

State before:
case inl
hw : 1 ∈ {z | z = 1 ∨ ζ z ≠ 0}
⊢ ζ₁ 1 ≠ 0
Tactic:
simp only [ζ₁, Function.update_same, ne_eq, one_ne_zero, not_false_eq_true]
State after:
no goals

State before:
case inr
w : ℂ
hw : w ∈ {z | z = 1 ∨ ζ z ≠ 0}
hw' : w ≠ 1
⊢ ζ₁ w ≠ 0
Tactic:
simp only [ne_eq, Set.mem_setOf_eq, hw', false_or] at hw
State after:
case inr
w : ℂ
hw' : w ≠ 1
hw : ¬ζ w = 0
⊢ ζ₁ w ≠ 0

State before:
case inr
w : ℂ
hw' : w ≠ 1
hw : ¬ζ w = 0
⊢ ζ₁ w ≠ 0
Tactic:
simp only [ζ₁, ne_eq, hw', not_false_eq_true, Function.update_noteq, _root_.mul_eq_zero, hw,
  false_or]
State after:
case inr
w : ℂ
hw' : w ≠ 1
hw : ¬ζ w = 0
⊢ ¬w - 1 = 0

State before:
case inr
w : ℂ
hw' : w ≠ 1
hw : ¬ζ w = 0
⊢ ¬w - 1 = 0
Tactic:
exact sub_ne_zero.mpr hw'
State after:
no goals