-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right {u v u' v' : ℝ → A}
    (hu : ContinuousOn u [[a, b]])
    (hv : ContinuousOn v [[a, b]])
    (huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x)
    (hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x)
    (hu' : IntervalIntegrable u' volume a b)
    (hv' : IntervalIntegrable v' volume a b) :
    ∫ x in a..b, u x * v' x = u b * v b - u a * v a - ∫ x in a..b, u' x * v x

Proof state:
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Tactic:
rw [← integral_deriv_mul_eq_sub_of_hasDeriv_right hu hv huu' hvv' hu' hv', ← integral_sub]

Result:
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x * v' x = ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x - u' x * v x

case hf
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x => u' x * v x + u x * v' x) volume a b

case hg
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x => u' x * v x) volume a b

Proof state:
case hg
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x => u' x * v x) volume a b

Tactic:
exact hu'.mul_continuousOn hv

Result:
no goals

Proof state:
case hf
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x => u' x * v x + u x * v' x) volume a b

Tactic:
exact (hu'.mul_continuousOn hv).add (hv'.continuousOn_mul hu)

Result:
no goals

Proof state:
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x * v' x = ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x - u' x * v x

Tactic:
simp_rw [add_sub_cancel_left]

Result:
no goals