-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
@[simp]
lemma hurwitzEvenFEPair_zero_symm :
    (hurwitzEvenFEPair 0).symm = hurwitzEvenFEPair 0

Proof state:
⊢ (hurwitzEvenFEPair 0).symm = hurwitzEvenFEPair 0

Tactic:
unfold hurwitzEvenFEPair WeakFEPair.symm

Result:
⊢ {
      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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5,
              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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }

Proof state:
⊢ {
      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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5,
              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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5,
            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_4, hε := hurwitzEvenFEPair.proof_5, h_feq := ⋯,
      hf_top := ⋯, hg_top := ⋯ }

Tactic:
congr 1 <;> simp [evenKernel_eq_cosKernel_of_zero]

Result:
no goals