-- Module: Mathlib.NumberTheory.LSeries.DirichletContinuation
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)
calc :
  completedLFunction χ (1 - s) =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s
calc₁ :
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N) ((𝓕 : (a : ZMod N → ℂ) → ZMod N → ℂ) (⇑χ : (a : ZMod N) → ℂ)) s =
    HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N)
        (fun (j : ZMod N) ↦
          HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
            ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ))
        s
calc₂ :
  HMul.hMul (β := ℂ) (HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1)) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) / ε *
      ZMod.completedLFunction (N := N)
        (fun (j : ZMod N) ↦
          HMul.hMul (β := ℂ) (HMul.hMul (α := ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) (gaussSum χ stdAddChar))
            ((χ⁻¹ : (a : ZMod N) → ℂ) j : ℂ))
        s =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s *
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ)
calc₃ :
  HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s *
      HMul.hMul (α := ℂ) (β := ℂ) ((χ : (a : ZMod N) → ℂ) (-1) : ℂ) ((χ⁻¹ : (a : ZMod N) → ℂ) (-1) : ℂ) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s
⊢ completedLFunction χ (1 - s) =
    HPow.hPow (α := ℂ) (↑N : ℂ) (s - 1) / HPow.hPow (β := ℕ) I (if χ.Even then 0 else 1) * gaussSum χ stdAddChar *
      completedLFunction χ⁻¹ s

Tactic:
calc completedLFunction χ (1 - s)
  _ = N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 χ) s := by
    simp only [ε]
    split_ifs with h
    · rw [pow_zero, div_one, h, mul_one, completedLFunction,
        completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]
    · replace h : χ.Odd := χ.even_or_odd.resolve_left h
      rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun,
        pow_one, h, div_I, mul_neg_one, ← neg_mul, neg_neg]
  _ = (_) * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s := by
    congr 2 with j
    rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s * (χ (-1) * χ⁻¹ (-1)) := by
    rw [completedLFunction, completedLFunction_const_mul]
    ring
  _ = N ^ (s - 1) / ε * gaussSum χ stdAddChar * completedLFunction χ⁻¹ s := by
    rw [← MulChar.mul_apply, mul_inv_cancel, MulChar.one_apply (isUnit_one.neg), mul_one]

Premises used: ZMod.completedLFunction, DirichletCharacter.completedLFunction, HMul.hMul, ZMod.stdAddChar, ZMod.dft, HSub.hSub, Inv.inv, gaussSum, OfNat.ofNat, DFunLike.coe, Neg.neg