rw [Int.floor_natCast, Int.floor_natCast, ← intervalIntegral.integral_const_mul]
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) =
    (∫ (x : ℝ) in ↑a..↑b, φ x) + (↑⌊↑b⌋ + 1 / 2 - ↑↑b) * φ ↑b - (↑⌊↑a⌋ + 1 / 2 - ↑↑a) * φ ↑a -
      ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    (∫ (x : ℝ) in ↑a..↑b, φ x) + (↑↑b + 1 / 2 - ↑↑b) * φ ↑b - (↑↑a + 1 / 2 - ↑↑a) * φ ↑a -
      ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x