ι : Type ?u.1886564
𝕜 : Type ?u.1886567
E : Type ?u.1886570
F : Type ?u.1886573
A : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt v (v' 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
ι : Type ?u.1886564
𝕜 : Type ?u.1886567
E : Type ?u.1886570
F : Type ?u.1886573
A : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt v (v' 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
ι : Type ?u.1886564
𝕜 : Type ?u.1886567
E : Type ?u.1886570
F : Type ?u.1886573
A : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt v (v' x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x => u' x * v x) volume a b
ι : Type ?u.1886564
𝕜 : Type ?u.1886567
E : Type ?u.1886570
F : Type ?u.1886573
A : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt v (v' 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
rw [← integral_deriv_mul_eq_sub hu hv hu' hv', ← integral_sub]
no goals
ι : Type ?u.1886564
𝕜 : Type ?u.1886567
E : Type ?u.1886570
F : Type ?u.1886573
A : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt v (v' 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
exact integral_congr fun x _ => by simp only [add_sub_cancel']
no goals
ι : Type ?u.1886564
𝕜 : Type ?u.1886567
E : Type ?u.1886570
F : Type ?u.1886573
A : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt v (v' x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ u x * v' x = u' x * v x + u x * v' x - u' x * v x
simp only [add_sub_cancel']
no goals
case hf
ι : Type ?u.1886564
𝕜 : Type ?u.1886567
E : Type ?u.1886570
F : Type ?u.1886573
A : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt v (v' 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
exact
  (hu'.mul_continuousOn (HasDerivAt.continuousOn hv)).add
    (hv'.continuousOn_mul (HasDerivAt.continuousOn hu))
no goals
case hg
ι : Type ?u.1886564
𝕜 : Type ?u.1886567
E : Type ?u.1886570
F : Type ?u.1886573
A : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
a b : ℝ
u v u' v' : ℝ → A
hu : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), x ∈ [[a, b]] → HasDerivAt v (v' x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x => u' x * v x) volume a b
exact hu'.mul_continuousOn (HasDerivAt.continuousOn hv)