show ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖
case refine_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
⊢ y ∈
    {x_1 |
      (fun x_2 =>
          (Norm.norm ∘ fun y => f x (↑σ + ↑y * I)) x_2 = (Norm.norm ∘ (fun y => f x (↑σ + ↑y * I)) ∘ Neg.neg) x_2)
        x_1}
case refine_1
x σ σ' σ'' T : ℝ
xpos : 0 < x
σ_ne_zero : σ ≠ 0
σ_ne_neg_one : σ ≠ -1
this : Continuous fun y => f x (↑σ + ↑y * I)
y : ℝ
⊢ ‖f x (↑σ + ↑y * I)‖ = ‖f x (↑σ + ↑(-y) * I)‖