simp_rw [hfun_eq, MeasureTheory.integral_mul_left,
  Measure.integral_comp_mul_left (fun t ↦ (1 + t ^ 2)⁻¹) (a:=c.sqrt⁻¹)]
x σ σ' σ'' T c : ℝ
hc : 0 < c
hfun_eq : ∀ (t : ℝ), 1 / (c + t ^ 2) = c⁻¹ * (1 + ((√c)⁻¹ * t) ^ 2)⁻¹
⊢ 0 < ∫ (t : ℝ), 1 / (c + t ^ 2)
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)⁻¹