awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
apply : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
apply₁ : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ C + 1
apply₂ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ C + 1) μ a b
apply₃ : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

Tactic:
apply tendsto_integral_filter_of_dominated_convergence (bound := fun _ ↦ C + 1)

Premises used: intervalIntegral.tendsto_integral_filter_of_dominated_convergence, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))

Tactic:
hF.mono fun i hi ↦ hi.mono uIoc_subset_uIcc |>.aestronglyMeasurable measurableSet_uIoc

Premises used: Set.uIoc_subset_uIcc, ContinuousOn.aestronglyMeasurable, measurableSet_uIoc, Filter.Eventually.mono, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))

Tactic:
exact hF.mono fun i hi ↦ hi.mono uIoc_subset_uIcc |>.aestronglyMeasurable measurableSet_uIoc

Premises used: Set.uIoc_subset_uIcc, ContinuousOn.aestronglyMeasurable, measurableSet_uIoc, Filter.Eventually.mono, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))

Tactic:
case hF_meas =>
    exact hF.mono fun i hi ↦ hi.mono uIoc_subset_uIcc |>.aestronglyMeasurable measurableSet_uIoc

Premises used: Set.uIoc_subset_uIcc, ContinuousOn.aestronglyMeasurable, measurableSet_uIoc, Filter.Eventually.mono, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ C < C + 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ ∀ x ∈ [[a, b]], (norm ∘ f) x ≤ C

Tactic:
simpa [upperBounds] using hC

Premises used: upperBounds
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ ∀ᶠ (i : ι) in l, ∀ x ∈ [[a, b]], (norm ∘ F i) x ≤ C + 1

Tactic:
have := uniformContinuous_norm.comp_tendstoUniformlyOn h_lim
      |>.eventually_forall_le (show C < C + 1 by simp) (by simpa [upperBounds] using hC)
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
this : ∀ᶠ (i : ι) in l, ∀ x ∈ [[a, b]], (norm ∘ F i) x ≤ C + 1
⊢ ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ C + 1

Tactic:
this.mono fun i hi ↦ .of_forall fun x hx ↦ hi x <| uIoc_subset_uIcc hx

Premises used: Set.uIoc_subset_uIcc, Filter.Eventually.of_forall, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
this : ∀ᶠ (i : ι) in l, ∀ x ∈ [[a, b]], (norm ∘ F i) x ≤ C + 1
⊢ ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ C + 1

Tactic:
exact this.mono fun i hi ↦ .of_forall fun x hx ↦ hi x <| uIoc_subset_uIcc hx

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ C + 1

Tactic:
case h_bound =>
    have := uniformContinuous_norm.comp_tendstoUniformlyOn h_lim
      |>.eventually_forall_le (show C < C + 1 by simp) (by simpa [upperBounds] using hC)
    exact this.mono fun i hi ↦ .of_forall fun x hx ↦ hi x <| uIoc_subset_uIcc hx
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ C + 1) μ a b

Tactic:
intervalIntegrable_const

Premises used: intervalIntegrable_const
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ C + 1) μ a b

Tactic:
exact intervalIntegrable_const

Premises used: intervalIntegrable_const
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ C + 1) μ a b

Tactic:
case bound_integrable =>
    exact intervalIntegrable_const

Premises used: intervalIntegrable_const
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))

Tactic:
.of_forall fun x hx ↦ h_lim.tendsto_at <| uIoc_subset_uIcc hx

Premises used: TendstoUniformlyOn.tendsto_at, Set.uIoc_subset_uIcc, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))

Tactic:
exact .of_forall fun x hx ↦ h_lim.tendsto_at <| uIoc_subset_uIcc hx
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C
⊢ ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))

Tactic:
case h_lim =>
    exact .of_forall fun x hx ↦ h_lim.tendsto_at <| uIoc_subset_uIcc hx
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
inst_2 : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.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)
simp :
  ∀ (h_bound : ∀ (n : ι), ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound n x)
    (bound_summable : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Summable (α := ℝ) fun (n : ι) ↦ bound n x)
    (bound_integrable : IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ∑' (n : ι), bound n t) (Ι a b) μ)
    (h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasSum (fun (n : ι) ↦ F n x) (f x)),
    HasSum (fun (n : ι) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F n t ∂μ))
      (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, f t ∂μ))
⊢ HasSum.{u_2, u_3} (α := E) (fun (n : ι) ↦ ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)

Tactic:
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc, ←
    ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *

Premises used: intervalIntegrable_iff, intervalIntegral.intervalIntegral_eq_integral_uIoc, measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
inst_2 : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound n x
bound_summable : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Summable (α := ℝ) fun (n : ι) ↦ bound n x
bound_integrable : IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ∑' (n : ι), bound n t) (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasSum (fun (n : ι) ↦ F n x) (f x)
⊢ HasSum (fun (n : ι) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F n t ∂μ))
    (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, f t ∂μ))

Tactic:
(hasSum_integral_of_dominated_convergence bound hF_meas h_bound bound_summable bound_integrable
          h_lim).const_smul
      _

Premises used: MeasureTheory.hasSum_integral_of_dominated_convergence, HasSum.const_smul
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
inst_2 : Countable ι
F : ι → ℝ → E
bound : ι → ℝ → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ (n : ι), ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound n x
bound_summable : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Summable (α := ℝ) fun (n : ι) ↦ bound n x
bound_integrable : IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ∑' (n : ι), bound n t) (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasSum (fun (n : ι) ↦ F n x) (f x)
⊢ HasSum (fun (n : ι) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, F n t ∂μ))
    (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (t : ℝ) in Ι a b, f t ∂μ))

Tactic:
exact
    (hasSum_integral_of_dominated_convergence bound hF_meas h_bound bound_summable bound_integrable
          h_lim).const_smul
      _
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
pos :
  ∀ (hE : CompleteSpace E),
    HasSum.{u_2, u_1} (α := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a..b, (f i : (a : ℝ) → E) x)
      (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i : (a : ℝ) → E) x)
neg :
  ∀ (hE : ¬CompleteSpace E),
    HasSum.{u_2, u_1} (α := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a..b, (f i : (a : ℝ) → E) x)
      (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i : (a : ℝ) → E) x)
⊢ HasSum.{u_2, u_1} (α := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a..b, (f i : (a : ℝ) → E) x)
    (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i : (a : ℝ) → E) x)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : ¬CompleteSpace E
⊢ HasSum.{u_2, u_1} (α := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a..b, (f i : (a : ℝ) → E) x)
    (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i : (a : ℝ) → E) x)

Tactic:
simp [intervalIntegral, integral, hE, hasSum_zero]

Premises used: intervalIntegral, hasSum_zero, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
pos :
  ∀ (n : ι),
    ∀ᵐ (t : ℝ),
      t ∈ Ι a b →
        norm (E := E) ((f n : (a : ℝ) → E) t : E) ≤
          ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f n)‖
pos₁ :
  ∀ᵐ (t : ℝ),
    t ∈ Ι a b →
      Summable (α := ℝ) fun (n : ι) ↦
        ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f n)‖
pos₂ :
  IntervalIntegrable (ε := ℝ)
    (fun (t : ℝ) ↦
      ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f n)‖)
    volume a b
pos₃ :
  ∀ᵐ (t : ℝ),
    t ∈ Ι a b → HasSum.{u_2, u_1} (α := E) (fun (n : ι) ↦ (f n : (a : ℝ) → E) t) (∑' (i : ι), (f i : (a : ℝ) → E) t)
⊢ HasSum.{u_2, u_1} (α := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a..b, (f i : (a : ℝ) → E) x)
    (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i : (a : ℝ) → E) x)

Tactic:
apply hasSum_integral_of_dominated_convergence
    (fun i (x : ℝ) => ‖(f i).restrict ↑(⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ)‖)
    (fun i => (map_continuous <| f i).aestronglyMeasurable)

Premises used: Norm.norm, intervalIntegral.hasSum_integral_of_dominated_convergence, ContinuousMapClass.map_continuous, Continuous.aestronglyMeasurable, ContinuousMap.restrict
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
i : ι
pos :
  ∀ (x : ℝ) (hx : x ∈ Ι a b),
    norm (E := E) ((f i : (a : ℝ) → E) x : E) ≤
      ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι a b →
      norm (E := E) ((f i : (a : ℝ) → E) t : E) ≤
        ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖

Tactic:
filter_upwards with x hx
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
i : ι
x : ℝ
hx : x ∈ Ι a b
apply : x ∈ (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ)
⊢ norm (E := E) ((f i : (a : ℝ) → E) x : E) ≤
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖

Tactic:
apply ContinuousMap.norm_coe_le_norm ((f i).restrict _) ⟨x, _⟩

Premises used: ContinuousMap.norm_coe_le_norm, Subtype.mk, ContinuousMap.restrict
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
i : ι
x : ℝ
hx : x ∈ Ι a b
⊢ x ∈ (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ)

Tactic:
⟨hx.1.le, hx.2⟩

Premises used: Set.Mem, setOf, LT.lt.le, Set.Icc, And.right, And.left, And.intro, Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
i : ι
x : ℝ
hx : x ∈ Ι a b
⊢ x ∈ (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ)

Tactic:
exact ⟨hx.1.le, hx.2⟩
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι a b →
      Summable (α := ℝ) fun (n : ι) ↦
        ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f n)‖

Tactic:
ae_of_all _ fun x _ => hf_sum

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι a b →
      Summable (α := ℝ) fun (n : ι) ↦
        ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f n)‖

Tactic:
exact ae_of_all _ fun x _ => hf_sum

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
⊢ IntervalIntegrable (ε := ℝ)
    (fun (t : ℝ) ↦
      ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f n)‖)
    volume a b

Tactic:
intervalIntegrable_const

Premises used: intervalIntegrable_const
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
⊢ IntervalIntegrable (ε := ℝ)
    (fun (t : ℝ) ↦
      ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f n)‖)
    volume a b

Tactic:
exact intervalIntegrable_const

Premises used: intervalIntegrable_const
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι a b → HasSum.{u_2, u_1} (α := E) (fun (n : ι) ↦ (f n : (a : ℝ) → E) t) (∑' (i : ι), (f i : (a : ℝ) → E) t)

Tactic:
ae_of_all _ fun x hx => Summable.hasSum ?_

Premises used: Summable.hasSum, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
pos : ∀ (x : ℝ) (hx : x ∈ Ι a b), Summable.{u_2, u_1} (α := E) fun (n : ι) ↦ (f n : (a : ℝ) → E) x
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι a b → HasSum.{u_2, u_1} (α := E) (fun (n : ι) ↦ (f n : (a : ℝ) → E) t) (∑' (i : ι), (f i : (a : ℝ) → E) t)

Tactic:
refine ae_of_all _ fun x hx => Summable.hasSum ?_

Premises used: Summable.hasSum, MeasureTheory.ae_of_all