apply intervalIntegral.integral_congr_ae
case h.e'_3.h.e'_6
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
case h.e'_3.h.e'_6.h
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x