-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
s : ℂ
e_a :
  (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - 1 / s
e_a₁ :
  { f := (hurwitzEvenFEPair a).g, g := (hurwitzEvenFEPair a).f, k := (hurwitzEvenFEPair a).k,
              ε := (hurwitzEvenFEPair a).ε⁻¹, f₀ := (hurwitzEvenFEPair a).g₀, g₀ := (hurwitzEvenFEPair a).f₀,
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      (1 / (s / 2)) •
          { f := (hurwitzEvenFEPair a).g, g := (hurwitzEvenFEPair a).f, k := (hurwitzEvenFEPair a).k,
              ε := (hurwitzEvenFEPair a).ε⁻¹, f₀ := (hurwitzEvenFEPair a).g₀, g₀ := (hurwitzEvenFEPair a).f₀,
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.f₀ /
        2 =
    { f := (hurwitzEvenFEPair a).g, g := (hurwitzEvenFEPair a).f, k := (hurwitzEvenFEPair a).k,
              ε := (hurwitzEvenFEPair a).ε⁻¹, f₀ := (hurwitzEvenFEPair a).g₀, g₀ := (hurwitzEvenFEPair a).f₀,
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / s
e_a₂ :
  {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      (1 / (s / 2)) •
          {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.f₀ /
        2 =
    {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / s
e_a₃ :
  {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / (s / 2) *
          {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.f₀ /
        2 =
    {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / s
e_a₄ :
  {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / (s / 2) / 2 =
    {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / s
e_a₅ :
  {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / (s / 2 * 2) =
    {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / s
e_a₆ e_a₇ :
  {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / s =
    {
              f :=
                WeakFEPair.g
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g :=
                WeakFEPair.f
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              k :=
                WeakFEPair.k
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              ε :=
                (WeakFEPair.ε
                    { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                      f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                      hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ })⁻¹,
              f₀ :=
                WeakFEPair.g₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              g₀ :=
                WeakFEPair.f₀
                  { f := ofReal ∘ evenKernel a, g := ofReal ∘ cosKernel a, k := 1 / 2, ε := 1,
                    f₀ := if a = 0 then 1 else 0, g₀ := 1, hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ },
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ : WeakFEPair ℂ }.Λ₀
          (s / 2) /
        2 -
      1 / s
⊢ (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    completedCosZeta₀ a s - 1 / s

Tactic:
rw [completedCosZeta₀, WeakFEPair.symm, hurwitzEvenFEPair, smul_eq_mul, mul_one, div_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ)]

Premises used: div_mul_cancel₀, HurwitzZeta.completedCosZeta₀, two_ne_zero', smul_eq_mul, div_div, mul_one, Complex, WeakFEPair.symm, HurwitzZeta.hurwitzEvenFEPair