-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
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
⊢ (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    completedCosZeta₀ a s - 1 / s
have 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : WeakFEPair ℂ },
            hf_int := sorry, hg_int := sorry, hk := sorry, hε := sorry, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : WeakFEPair ℂ },
            hf_int := sorry, hg_int := sorry, hk := sorry, hε := sorry, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                    hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : 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 := sorry, hg_int := sorry, hk := hurwitzEvenFEPair._proof_7,
                  hε := hurwitzEvenFEPair._proof_8, h_feq := sorry, hf_top := sorry, hg_top := sorry : WeakFEPair ℂ },
            hf_int := sorry, hg_int := sorry, hk := sorry, hε := sorry, h_feq := sorry, hf_top := sorry, hg_top := sorry : WeakFEPair ℂ }.Λ₀
        (s / 2) /
      2 -
    1 / s
Tactic: rw [completedCosZeta₀, WeakFEPair.symm, hurwitzEvenFEPair, smul_eq_mul, mul_one, div_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ)]