Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ { 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 := ⋯ }.Λ₀
          (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 := ⋯ }.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 := ⋯ }.Λ₀
          (s / 2) /
        2 -
      1 / s

Tactic:
hurwitzEvenFEPair,

Goal state after:
case e_a
a : UnitAddCircle
s : ℂ
⊢ {
              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 := ⋯ }.g,
              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 := ⋯ }.f,
              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 := ⋯ }.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 := ⋯ }.ε⁻¹,
              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 := ⋯ }.g₀,
              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 := ⋯ }.f₀,
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.Λ₀
          (s / 2) /
        2 -
      (1 / (s / 2)) •
          {
              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 := ⋯ }.g,
              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 := ⋯ }.f,
              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 := ⋯ }.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 := ⋯ }.ε⁻¹,
              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 := ⋯ }.g₀,
              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 := ⋯ }.f₀,
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.f₀ /
        2 =
    {
              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 := ⋯ }.g,
              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 := ⋯ }.f,
              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 := ⋯ }.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 := ⋯ }.ε⁻¹,
              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 := ⋯ }.g₀,
              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 := ⋯ }.f₀,
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.Λ₀
          (s / 2) /
        2 -
      1 / s