congr <;> simp only [Int.floor_natCast]
case h.e'_2
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]]
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s = ∑ n ∈ Finset.Ioc ⌊↑a⌋ ⌊↑b⌋, φ ↑n
no goals