-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem continuousOn_primitive (h_int : IntegrableOn f (Icc a b) μ) :
    ContinuousOn (fun x => ∫ t in Ioc a x, f t ∂μ) (Icc a b)

Proof state:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ IntegrableOn f (Ioc a b) μ

Tactic:
exact h_int.mono Ioc_subset_Icc_self le_rfl

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Tactic:
rw [continuousOn_congr this]

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Tactic:
by_cases h : a ≤ b

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : ¬a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Proof state:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : ¬a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Tactic:
rw [Icc_eq_empty h]

Result:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : ¬a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) ∅

Proof state:
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : ¬a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) ∅

Tactic:
exact continuousOn_empty _

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Tactic:
have : ∀ x ∈ Icc a b, ∫ t in Ioc a x, f t ∂μ = ∫ t in a..x, f t ∂μ := by
  intro x x_in
  simp_rw [integral_of_le x_in.1]

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
x : ℝ
x_in : x ∈ Icc a b
⊢ ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ

Tactic:
simp_rw [integral_of_le x_in.1]

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ IntervalIntegrable f μ (a ⊓ a) (a ⊔ b)

Tactic:
simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, min_eq_left, max_eq_right, h,
  min_self]

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ IntegrableOn f (Ioc a b) μ

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
⊢ ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ

Tactic:
intro x x_in

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
x : ℝ
x_in : x ∈ Icc a b
⊢ ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ

Proof state:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b)

Tactic:
intro x₀ _

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b) x₀

Proof state:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b) x₀

Tactic:
refine continuousWithinAt_primitive (measure_singleton x₀) ?_

Result:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ
x₀ : ℝ
a✝ : x₀ ∈ Icc a b
⊢ IntervalIntegrable f μ (a ⊓ a) (a ⊔ b)