ι✝ : Type ?u.17029728
𝕜 : Type ?u.17029731
E : Type u_2
F✝ : Type ?u.17029737
A : Type ?u.17029740
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (Measure.restrict μ (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ‖F n x‖ ≤ bound x
bound_integrable : IntegrableOn bound (Ι a b)
h_lim : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), Tendsto (fun n => F n x) l (𝓝 (f x))
⊢ Tendsto (fun n => (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, F n x ∂μ) l
    (𝓝 ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ))
ι✝ : Type ?u.17029728
𝕜 : Type ?u.17029731
E : Type u_2
F✝ : Type ?u.17029737
A : Type ?u.17029740
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (Measure.restrict μ (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun n => F n x) l (𝓝 (f x))
⊢ Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc,
  ← ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *
no goals
ι✝ : Type ?u.17029728
𝕜 : Type ?u.17029731
E : Type u_2
F✝ : Type ?u.17029737
A : Type ?u.17029740
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (Measure.restrict μ (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), ‖F n x‖ ≤ bound x
bound_integrable : IntegrableOn bound (Ι a b)
h_lim : ∀ᵐ (x : ℝ) ∂Measure.restrict μ (Ι a b), Tendsto (fun n => F n x) l (𝓝 (f x))
⊢ Tendsto (fun n => (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, F n x ∂μ) l
    (𝓝 ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ))
exact tendsto_const_nhds.smul <|
  tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_lim