Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: 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 * 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

Tactic:
div_mul_cancel₀ _ (two_ne_zero' ℂ)

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 =
    {
              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