ι✝ : Type ?u.17150684
𝕜 : Type ?u.17150687
E : Type u_2
F✝ : Type ?u.17150693
A : Type ?u.17150696
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
ι : Type u_1
inst✝ : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (Measure.restrict μ (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ‖F n x‖ ≤ bound n x
bound_summable : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), Summable fun n => bound n x
bound_integrable : IntegrableOn (fun t => ∑' (n : ι), bound n t) (Ι a b)
h_lim : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasSum (fun n => F n x) (f x)
⊢ HasSum (fun n => (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, F n x ∂μ)
    ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ)
ι✝ : Type ?u.17150684
𝕜 : Type ?u.17150687
E : Type u_2
F✝ : Type ?u.17150693
A : Type ?u.17150696
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
ι : Type u_1
inst✝ : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (Measure.restrict μ (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t
bound_summable : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Summable fun n => bound n t
bound_integrable : IntervalIntegrable (fun t => ∑' (n : ι), bound n t) μ a b
h_lim : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasSum (fun n => F n t) (f t)
⊢ HasSum (fun n => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc, ←
  ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *
no goals
ι✝ : Type ?u.17150684
𝕜 : Type ?u.17150687
E : Type u_2
F✝ : Type ?u.17150693
A : Type ?u.17150696
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
ι : Type u_1
inst✝ : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (Measure.restrict μ (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ‖F n x‖ ≤ bound n x
bound_summable : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), Summable fun n => bound n x
bound_integrable : IntegrableOn (fun t => ∑' (n : ι), bound n t) (Ι a b)
h_lim : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), HasSum (fun n => F n x) (f x)
⊢ HasSum (fun n => (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, F n x ∂μ)
    ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ)
exact
  (hasSum_integral_of_dominated_convergence bound hF_meas h_bound bound_summable bound_integrable
        h_lim).const_smul
    _