awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
apply₁ : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ C + 1
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
have apply₂ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ C + 1) μ 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))
apply₁ : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ C + 1
apply₂ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ C + 1) μ 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₃ : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))
Tactic: apply tendsto_integral_filter_of_dominated_convergence (bound := fun _ ↦ C + 1)
-- 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
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
have this : ∀ᶠ (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)
-- 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
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)
⊢ HasSum.{u_2, u_3} (α := E) (fun (n : ι) ↦ ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)
have 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 ∂μ))
Tactic: simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc, ←
    ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *
Cleared hypotheses: h_bound, bound_summable, 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 : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
⊢ 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)
have 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)
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
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)
⊢ 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)
have 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)
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
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)
have pos : ∀ (n : ι),
  ∀ᵐ (t : ℝ),
    t ∈ Ι a b →
      norm (E := E) ((f n : (a : ℝ) → E) t : E) ≤
        ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := sorry : Compacts ℝ } : Set ℝ) (f n)‖
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)
-- 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 : ℝ
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)‖
⊢ 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)
have pos₁ : ∀ᵐ (t : ℝ),
  t ∈ Ι a b →
    Summable (α := ℝ) fun (n : ι) ↦
      ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := sorry : Compacts ℝ } : Set ℝ) (f n)‖
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)
-- 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 : ℝ
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)‖
⊢ 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)
have pos₂ : IntervalIntegrable (ε := ℝ)
  (fun (t : ℝ) ↦
    ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := sorry : Compacts ℝ } : Set ℝ) (f n)‖)
  volume a b
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)
-- 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 : ℝ
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
⊢ 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)
have pos₃ : ∀ᵐ (t : ℝ),
  t ∈ Ι a b → HasSum.{u_2, u_1} (α := E) (fun (n : ι) ↦ (f n : (a : ℝ) → E) t) (∑' (i : ι), (f i : (a : ℝ) → E) t)
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)
-- 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 : ℝ
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 : ι
⊢ ∀ᵐ (t : ℝ),
    t ∈ Ι a b →
      norm (E := E) ((f i : (a : ℝ) → E) t : E) ≤
        ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
have pos : ∀ (x : ℝ) (hx : x ∈ Ι a b),
  norm (E := E) ((f i : (a : ℝ) → E) x : E) ≤
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := sorry : Compacts ℝ } : Set ℝ) (f i)‖
Tactic: filter_upwards 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
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
⊢ norm (E := E) ((f i : (a : ℝ) → E) x : E) ≤
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
have apply : x ∈ (↑{ carrier := [[a, b]], isCompact' := sorry : Compacts ℝ } : Set ℝ)
Tactic: apply ContinuousMap.norm_coe_le_norm ((f i).restrict _) ⟨x, _⟩
-- 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 : ℝ
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)
have pos : ∀ (x : ℝ) (hx : x ∈ Ι a b), Summable.{u_2, u_1} (α := E) fun (n : ι) ↦ (f n : (a : ℝ) → E) x
Tactic: refine ae_of_all _ fun x hx => Summable.hasSum ?_
-- 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
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
x_1 : ℝ
hx : x_1 ∈ Ι a b
x : ↥{ carrier := [[a, b]], isCompact' := ⋯ } :=
  Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Compacts ℝ) { carrier := [[a, b]], isCompact' := ⋯ } x) x_1 ⋯
⊢ Summable.{u_2, u_1} (α := E) fun (n : ι) ↦ (f n : (a : ℝ) → E) x_1
have this : Summable.{u_2, u_1} (α := C((↑(↑{ carrier := [[a, b]], isCompact' := sorry : Compacts ℝ } : Set ℝ) : Type), E))
  fun (i : ι) ↦ ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := sorry } : Set ℝ) (f i)
Tactic: have := hf_sum.of_norm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have pos : ∀ (h₀ : b₀ ∈ Icc b₁ b₂), ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
Tactic: by_cases h₀ : b₀ ∈ Icc b₁ b₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
pos :
  ∀ (h₀ : b₀ ∈ Icc b₁ b₂), ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have neg : ∀ (h₀ : b₀ ∉ Icc b₁ b₂), ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
Tactic: by_cases h₀ : b₀ ∈ Icc b₁ b₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have h₁₂ : b₁ ≤ b₂
Tactic: have h₁₂ : b₁ ≤ b₂ := h₀.1.trans h₀.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have min₁₂ : min b₁ b₂ = b₁
Tactic: have min₁₂ : min b₁ b₂ = b₁ := min_eq_left h₁₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ IntervalIntegrable f μ b₁ x
have apply : [[b₁, x]] ⊆ [[min a b₁, max a b₂]]
Tactic: apply h_int.mono_set
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ [[b₁, x]] ⊆ [[min a b₁, max a b₂]]
have h₃ : b₁ ∈ [[min a b₁, max a b₂]]
Tactic: apply uIcc_subset_uIcc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
h₃ : b₁ ∈ [[min a b₁, max a b₂]]
⊢ [[b₁, x]] ⊆ [[min a b₁, max a b₂]]
have h₄ : x ∈ [[min a b₁, max a b₂]]
Tactic: apply uIcc_subset_uIcc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
Tactic: have h_int' : ∀ {x}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x := by
      rintro x ⟨h₁, h₂⟩
      apply h_int.mono_set
      apply uIcc_subset_uIcc
      · exact ⟨min_le_of_left_le (min_le_right a b₁),
          h₁.trans (h₂.trans <| le_max_of_le_right <| le_max_right _ _)⟩
      · exact ⟨min_le_of_left_le <| (min_le_right _ _).trans h₁,
          le_max_of_le_right <| h₂.trans <| le_max_right _ _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..b, f x ∂μ)
have rw : IntervalIntegrable f μ a b₁
Tactic: rw [← integral_add_adjacent_intervals _ (h_int' ⟨h₁, h₂⟩)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ IntervalIntegrable f μ a b₁
have apply : [[a, b₁]] ⊆ [[min a b₁, max a b₂]]
Tactic: apply h_int.mono_set
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ [[a, b₁]] ⊆ [[min a b₁, max a b₂]]
have h₃ : a ∈ [[min a b₁, max a b₂]]
Tactic: apply uIcc_subset_uIcc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
h₃ : a ∈ [[min a b₁, max a b₂]]
⊢ [[a, b₁]] ⊆ [[min a b₁, max a b₂]]
have h₄ : b₁ ∈ [[min a b₁, max a b₂]]
Tactic: apply uIcc_subset_uIcc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have this : ∀ b ∈ Icc b₁ b₂,
  ∫ (x : ℝ) in a..b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..b, f x ∂μ)
Tactic: have : ∀ b ∈ Icc b₁ b₂,
        ∫ x in a..b, f x ∂μ = (∫ x in a..b₁, f x ∂μ) + ∫ x in b₁..b, f x ∂μ := by
      rintro b ⟨h₁, h₂⟩
      rw [← integral_add_adjacent_intervals _ (h_int' ⟨h₁, h₂⟩)]
      apply h_int.mono_set
      apply uIcc_subset_uIcc
      · exact ⟨min_le_of_left_le (min_le_left a b₁), le_max_of_le_right (le_max_left _ _)⟩
      · exact ⟨min_le_of_left_le (min_le_right _ _),
          le_max_of_le_right (h₁.trans <| h₂.trans (le_max_right a b₂))⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  ∀ b ∈ Icc b₁ b₂,
    ∫ (x : ℝ) in a..b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..b, f x ∂μ)
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have apply : ContinuousWithinAt.{0, u_1} (Y := E)
  (fun (y : ℝ) ↦ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..y, f x ∂μ)) (Icc b₁ b₂) b₀
Tactic: apply ContinuousWithinAt.congr _ this (this _ h₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ ContinuousWithinAt.{0, u_1} (Y := E)
    (fun (y : ℝ) ↦ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..y, f x ∂μ)) (Icc b₁ b₂) b₀
have refine : ContinuousWithinAt.{0, u_1} (Y := E) (fun (y : ℝ) ↦ ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
Tactic: refine continuousWithinAt_const.add ?_