convert intervalIntegral.integral_mul_deriv_eq_deriv_mul hu φDiff hu' hv' using 1
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hu' : IntervalIntegrable u' MeasureTheory.volume a b
hv' : IntervalIntegrable (deriv φ) MeasureTheory.volume a b
⊢ ∫ (x : ℝ) in a..b, (c - ↑x) * deriv φ x = (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x
case h.e'_3
φ : ℝ → ℂ
a b : ℝ
c : ℂ
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
u : ℝ → ℂ := fun x => c - ↑x
u' : ℝ → ℂ := fun x => -1
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hu' : IntervalIntegrable u' MeasureTheory.volume a b
hv' : IntervalIntegrable (deriv φ) MeasureTheory.volume a b
⊢ (c - ↑b) * φ b - (c - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x = u b * φ b - u a * φ a - ∫ (x : ℝ) in a..b, u' x * φ x