awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
f : ι → α → G
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ) ∞
hG : CompleteSpace G
hf'' : ∀ (i : ι), AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n a‖₊ : ℝ)
⊢ ∀ᵐ (a : α) ∂μ, HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ f n a) (∑' (i : ι), f i a)
have h : ∀ (x : α) (hx : Summable (α := ℝ) fun (n : ι) ↦ (↑‖f n x‖₊ : ℝ)),
  HasSum.{u_3, u_4} (α := G) (fun (n : ι) ↦ f n x) (∑' (i : ι), f i x)
Tactic: filter_upwards [hhh] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
⊢ HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
have pos : ∀ (hE : CompleteSpace E),
  HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
pos :
  ∀ (hE : CompleteSpace E),
    HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
⊢ HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
have neg : ∀ (hE : ¬CompleteSpace E),
  HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
have pos : HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∑' (i : ι), ∫ (a : α), F i a ∂μ)
Tactic: rw [integral_tsum (fun i ↦ (hF_int i).1)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
pos : HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∑' (i : ι), ∫ (a : α), F i a ∂μ)
⊢ HasSum.{u_2, u_4} (α := E) (fun (x : ι) ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)
have pos₁ : Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ) ∞
Tactic: rw [integral_tsum (fun i ↦ (hF_int i).1)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ∫⁻ (a : α), (↑‖F i a‖₊ : ℝ≥0∞) ∂μ = (↑(nnnorm (E := ℝ) (∫ (a : α), ‖F i a‖ ∂μ)) : ℝ≥0∞)
have rw : ENNReal.ofReal (∫ (a : α), (↑‖F i a‖₊ : ℝ) ∂μ) = ENNReal.ofReal (∫ (x : α), ‖F i x‖ ∂μ)
Tactic: rw [lintegral_coe_eq_integral _ (hF_int i).norm, coe_nnreal_eq, coe_nnnorm,
      Real.norm_of_nonneg (integral_nonneg (fun a ↦ norm_nonneg (F i a)))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ) ∞
have this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = enorm (E := ℝ) (∫ (a : α), ‖F i a‖ ∂μ)
Tactic: have (i : ι) : ∫⁻ a, ‖F i a‖ₑ ∂μ = ‖∫ a, ‖F i a‖ ∂μ‖ₑ := by
    dsimp [enorm]
    rw [lintegral_coe_eq_integral _ (hF_int i).norm, coe_nnreal_eq, coe_nnnorm,
      Real.norm_of_nonneg (integral_nonneg (fun a ↦ norm_nonneg (F i a)))]
    simp only [coe_nnnorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = enorm (E := ℝ) (∫ (a : α), ‖F i a‖ ∂μ)
⊢ Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ) ∞
have pos : Ne (α := ℝ≥0∞) (∑' (x : ι), enorm (E := ℝ) (∫ (a : α), ‖F x a‖ ∂μ)) ∞
Tactic: rw [funext this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → α → G
inst_3 : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∃ (C : ℝ), ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ C
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (n : ι) ↦ F n ω) l (𝓝 (f ω))
⊢ Tendsto.{u_4, u_3} (β := G) (fun (n : ι) ↦ ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))
have obtain : ∀ (c : ℝ) (h_boundc : ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ c),
  Tendsto.{u_4, u_3} (β := G) (fun (n : ι) ↦ ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))
Tactic: obtain ⟨c, h_boundc⟩ := h_bound
Cleared hypotheses: h_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
have h_int_eq : Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ
Tactic: have h_int_eq : (fun i => ∫ a in s i, f a ∂μ) = fun i => ∫ a, (s i).indicator f a ∂μ :=
    funext fun i => (integral_indicator (hsm i)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
have rw : Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
  (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
Tactic: rw [h_int_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
have rw : Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
  (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) f x ∂μ))
Tactic: rw [← integral_indicator (MeasurableSet.iInter hsm)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) f x ∂μ))
have refine_1 : ∀ (n : ℕ), AEStronglyMeasurable ((s n).indicator f) μ
Tactic: refine tendsto_integral_of_dominated_convergence bound ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
refine_1 : ∀ (n : ℕ), AEStronglyMeasurable ((s n).indicator f) μ
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) f x ∂μ))
have refine_2 : Integrable bound μ
Tactic: refine tendsto_integral_of_dominated_convergence bound ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
refine_1 : ∀ (n : ℕ), AEStronglyMeasurable ((s n).indicator f) μ
refine_2 : Integrable bound μ
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) f x ∂μ))
have refine_3 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖(s n).indicator f a‖ ≤ bound a
Tactic: refine tendsto_integral_of_dominated_convergence bound ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
refine_1 : ∀ (n : ℕ), AEStronglyMeasurable ((s n).indicator f) μ
refine_2 : Integrable bound μ
refine_3 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖(s n).indicator f a‖ ≤ bound a
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) f x ∂μ))
have refine_4 : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))
Tactic: refine tendsto_integral_of_dominated_convergence bound ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
⊢ AEStronglyMeasurable ((s n).indicator f) μ
have refine_1 : AEStronglyMeasurable f (μ.restrict (s n))
Tactic: rw [aestronglyMeasurable_indicator_iff (hsm n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ Integrable bound μ
have refine_2 : IntegrableOn (ε := ℝ) (fun (a : α) ↦ ‖f a‖) (s 0) μ
Tactic: rw [integrable_indicator_iff (hsm 0)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖(s n).indicator f a‖ ≤ bound a
have refine_3 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, (s n).indicator (fun (a : α) ↦ ‖f a‖) a ≤ bound a
Tactic: simp_rw [norm_indicator_eq_indicator_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, (s n).indicator (fun (a : α) ↦ ‖f a‖) a ≤ bound a
have refine_3 : ∀ (n : ℕ) (x : α), (s n).indicator (fun (a : α) ↦ ‖f a‖) x ≤ bound x
Tactic: refine fun n => Eventually.of_forall fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
x : α
⊢ (s n).indicator (fun (a : α) ↦ ‖f a‖) x ≤ bound x
have h₁ : 0 ≤ ‖f x‖
Tactic: grw [(h_anti zero_le).subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
x : α
h₁ : 0 ≤ ‖f x‖
⊢ (s n).indicator (fun (a : α) ↦ ‖f a‖) x ≤ bound x
have refine_3 : LE.le (α := ℝ) ((s 0).indicator (fun (a : α) ↦ ‖f a‖) x) ((s 0).indicator (fun (a : α) ↦ ‖f a‖) x)
Tactic: grw [(h_anti zero_le).subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))
have refine_4 : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α | (fun (a : α) ↦ Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))) x} a
Tactic: filter_upwards [] with a using le_trans (h_anti.tendsto_indicator _ _ _) (pure_le_nhds _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
refine_4 :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α | (fun (a : α) ↦ Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))) x}
      a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))
have refine_4₁ : ∀ (a : α), Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))
Tactic: filter_upwards [] with a using le_trans (h_anti.tendsto_indicator _ _ _) (pure_le_nhds _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.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.{u_3, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
have simp : ∀ (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound x)
  (bound_integrable : IntegrableOn bound (Ι a b) μ)
  (h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))),
  Tendsto (fun (n : ι) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, F n x ∂μ)) l
    (𝓝 (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ)))
Tactic: simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc,
    ← ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *
Cleared hypotheses: h_bound, bound_integrable, h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
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]]
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
have inl : ∀ [IsCountablyGenerated.{u_1} (α := ι) ⊥] (hF : ∀ᶠ (i : ι) in ⊥, ContinuousOn (F i) [[a, b]])
  (h_lim : TendstoUniformlyOn F f ⊥ [[a, b]]),
  Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) ⊥ (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
Tactic: rcases l.eq_or_neBot with rfl | hl
Cleared hypotheses: l, inst_2, hF, h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
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]]
inl :
  ∀ [IsCountablyGenerated.{u_1} (α := ι) ⊥] (hF : ∀ᶠ (i : ι) in ⊥, ContinuousOn (F i) [[a, b]])
    (h_lim : TendstoUniformlyOn F f ⊥ [[a, b]]),
    Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) ⊥ (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
have inr : ∀ (hl : l.NeBot),
  Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
Tactic: rcases l.eq_or_neBot with rfl | hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
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
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
have inr : ∀ (C : ℝ) (hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C),
  Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
Tactic: rcases isCompact_uIcc.bddAbove_image (h_lim.continuousOn hF.frequently).norm with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
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
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
have apply : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
Tactic: apply tendsto_integral_filter_of_dominated_convergence (bound := fun _ ↦ C + 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
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))
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
have apply₁ : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ C + 1
Tactic: apply tendsto_integral_filter_of_dominated_convergence (bound := fun _ ↦ C + 1)