any_goals norm_cast; simp only [one_div, add_sub_cancel_left]
case h.e'_3.e_a.e_a.e_a.e_a
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]]
⊢ 1 / 2 = ↑↑b + 1 / 2 - ↑↑b

case h.e'_3.e_a.e_a.e_a
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]]
⊢ 1 / 2 = ↑↑a + 1 / 2 - ↑↑a

case h.e'_3.e_a
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]]
⊢ ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
case h.e'_3.e_a
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]]
⊢ ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1))) = -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 2⁻¹ - ↑x) * deriv φ x