Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: ⊢ {
      f :=
        { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 := ⋯ }

Tactic:
congr 1

Goal state after:
case e_f
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 =
    ofReal ∘ evenKernel 0

case e_g
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 =
    ofReal ∘ cosKernel 0

case e_ε
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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 := ⋯ }.ε⁻¹ =
    1

case e_f₀
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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₀ =
    if 0 = 0 then 1 else 0

case e_g₀
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 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₀ =
    1