-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem continuous_primitive (h_int : ∀ a b, IntervalIntegrable f μ a b) (a : ℝ) :
    Continuous fun b => ∫ x in a..b, f x ∂μ

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ : ℝ
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀

Tactic:
obtain ⟨b₁, hb₁⟩ := exists_lt b₀

Result:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀

Proof state:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
b₂ : ℝ
hb₂ : b₀ < b₂
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀

Tactic:
apply ContinuousWithinAt.continuousAt _ (Icc_mem_nhds hb₁ hb₂)

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
b₂ : ℝ
hb₂ : b₀ < b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
b₂ : ℝ
hb₂ : b₀ < b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
exact continuousWithinAt_primitive (measure_singleton b₀) (h_int _ _)

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a : ℝ
⊢ Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
rw [continuous_iff_continuousAt]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a : ℝ
⊢ ∀ (x : ℝ), ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) x

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a : ℝ
⊢ ∀ (x : ℝ), ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) x

Tactic:
intro b₀

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ : ℝ
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀

Proof state:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀

Tactic:
obtain ⟨b₂, hb₂⟩ := exists_gt b₀

Result:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
b₂ : ℝ
hb₂ : b₀ < b₂
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀