-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.DirichletContinuation (goal)
Goal:
N : ℕ
inst : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : Eq (α := ℂ) (∑ j : ZMod N, (χ : (a : ZMod N) → ℂ) j) 0
ε : ℂ := HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1)
h : χ.Odd
neg :
  ZMod.completedLFunction (N := N) (⇑χ : (a : ZMod N) → ℂ) (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I 1 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₁ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I 1 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₂ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₃ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * -1 / I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₄ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    -(HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * -1 * I) *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₅ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    -(-HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I) *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
neg₆ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    - -HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
⊢ completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) /
        HPow.hPow (β := ℕ) I 1 *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
have neg₇ : HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
    ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) * I *
    ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
Tactic: rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun,
        pow_one, h, div_I, mul_neg_one, ← neg_mul, neg_neg]