-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.PrimesInAP (goal)
Goal:
q : ℕ
a : ZMod q
inst : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
classical :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    HMul.hMul (α := ℂ) ((1 : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s) +
        ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s) +
      1 / (s - 1)
classical₁ :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    1 * (deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s) +
        ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s) +
      1 / (s - 1)
classical₂ :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s +
        ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s) +
      1 / (s - 1)
classical₃ classical₄ classical₅ :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1) +
      ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s)
classical₆ :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ x ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((x : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction x) s / LFunction x s) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1) +
      ∑ i ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((i : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction i) s / LFunction i s)
classical₇ :
  deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)
classical₈ :
  ∀ (hs₁ : s ≠ 1),
    deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s =
      deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
      ∑ χ ∈ {1}ᶜ, HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s) / LFunction χ s =
    ∑ χ : DirichletCharacter ℂ q,
        HMul.hMul (α := ℂ) ((χ : (a : ZMod q) → ℂ) a⁻¹ : ℂ) (deriv (LFunction χ) s / LFunction χ s) +
      1 / (s - 1)
have classical₉ : ∀ (hs₁ : s ≠ 1),
  deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s +
      LFunction (N := q) 1 s / ((s - 1) * LFunction (N := q) 1 s) =
    deriv (LFunction (N := q) 1) s / LFunction (N := q) 1 s + 1 / (s - 1)
Tactic: classical -- for `Fintype.sum_eq_add_sum_compl`
  rw [Fintype.sum_eq_add_sum_compl 1, MulChar.one_apply ha', one_mul, add_right_comm]
  simp only [mul_div_assoc]
  congrm (?_ + _)
  have hs₁ : s ≠ 1 := fun h ↦ ((h ▸ hs).trans_eq one_re).false
  rw [deriv_LFunctionTrivChar₁_apply_of_ne_one _ hs₁, LFunctionTrivChar₁,
    Function.update_of_ne hs₁, LFunctionTrivChar, add_div,
    mul_div_mul_left _ _ (sub_ne_zero_of_ne hs₁)]
  conv_lhs => enter [2, 1]; rw [← mul_one (LFunction ..)]
  rw [mul_comm _ 1, mul_div_mul_right _ _ <| LFunction_ne_zero_of_one_le_re 1 (.inr hs₁) hs.le]