-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
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
rw₅ 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

Tactic:
rw [this, Left.sign_neg, abs_neg, SignType.coe_neg, neg_div, neg_div]

Premises used: abs_neg, neg_div, SignType.coe_neg, Left.sign_neg