Theorem: integrability_aux (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b : ℝ
⊢ IntervalIntegrable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) MeasureTheory.volume a b
Tactic:
convert integrability_aux₁.add integrability_aux₂ using 2
State after:
case h.e'_3.h
a b x✝ : ℝ
⊢ ↑⌊x✝⌋ + 1 / 2 - ↑x✝ = ↑⌊x✝⌋ + (1 / 2 - ↑x✝)

State before:
case h.e'_3.h
a b x✝ : ℝ
⊢ ↑⌊x✝⌋ + 1 / 2 - ↑x✝ = ↑⌊x✝⌋ + (1 / 2 - ↑x✝)
Tactic:
ring
State after:
no goals