-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaOdd (goal)
Goal:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)
rw :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))) : ℂ) /
          (↑|(-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))| : ℂ) ^ s /
        2
rw₁ :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑(-(SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|(-(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a))| : ℂ) ^ s /
        2
rw₂ :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑(-(SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2
rw₃ :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -(↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2
rw₄ :
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s) /
        2
⊢ (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
            (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
          2) =
    (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
      (↑((SignType.sign : (a : ℝ) → SignType) (-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a)) : ℂ) /
          (↑|-HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + a| : ℂ) ^ s /
        2
have rw₅ : (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2) =
  (↑((SignType.sign : (a : ℝ) → SignType) ((↑n : ℝ) + a)) : ℂ) / (↑|(↑n : ℝ) + a| : ℂ) ^ s / 2 +
    -((↑((SignType.sign : (a : ℝ) → SignType) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a)) : ℂ) /
          (↑|HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - a| : ℂ) ^ s /
        2)
Tactic: rw [this, Left.sign_neg, abs_neg, SignType.coe_neg, neg_div, neg_div]