simp [abs_eq_self.mpr <| Real.sqrt_nonneg c,
  mul_pos (inv_pos.mpr hc) <| mul_pos (sqrt_pos.mpr hc) Real.pi_pos]
x σ σ' σ'' T c : ℝ
hc : 0 < c
hfun_eq : ∀ (t : ℝ), 1 / (c + t ^ 2) = c⁻¹ * (1 + ((√c)⁻¹ * t) ^ 2)⁻¹
⊢ 0 < c⁻¹ * |(√c)⁻¹⁻¹| • ∫ (y : ℝ), (1 + y ^ 2)⁻¹
no goals