-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem continuousAt_parametric_primitive_of_dominated [FirstCountableTopology X]
    {F : X → ℝ → E} (bound : ℝ → ℝ) (a b : ℝ)
    {a₀ b₀ : ℝ} {x₀ : X} (hF_meas : ∀ x, AEStronglyMeasurable (F x) (μ.restrict <| Ι a b))
    (h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ t ∂μ.restrict <| Ι a b, ‖F x t‖ ≤ bound t)
    (bound_integrable : IntervalIntegrable bound μ a b)
    (h_cont : ∀ᵐ t ∂μ.restrict <| Ι a b, ContinuousAt (fun x ↦ F x t) x₀) (ha₀ : a₀ ∈ Ioo a b)
    (hb₀ : b₀ ∈ Ioo a b) (hμb₀ : μ {b₀} = 0) :
    ContinuousAt (fun p : X × ℝ ↦ ∫ t : ℝ in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)

Proof state:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
⊢ ∀ (x : X × ℝ),
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x.1 t‖ ≤ bound t) ∧ a < x.2 ∧ x.2 < b →
      ‖∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ‖ ≤ |∫ (s : ℝ) in b₀..x.2, 2 * bound s ∂μ|

Tactic:
rintro ⟨x, t⟩ ⟨hx : ∀ᵐ t ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t, ht : t ∈ Ioo a b⟩

Result:
case mk.intro
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
⊢ ‖∫ (s : ℝ) in b₀..(x, t).2, F (x, t).1 s - F x₀ s ∂μ‖ ≤ |∫ (s : ℝ) in b₀..(x, t).2, 2 * bound s ∂μ|

Proof state:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
this : Tendsto (fun x => ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ) (𝓝 (x₀, b₀)) (𝓝 0)
⊢ ContinuousAt (fun x => ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ) (x₀, b₀)

Tactic:
simpa [ContinuousAt]

Result:
no goals

Proof state:
case mk.intro.hbc
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
hiF :
  ∀ {x : X} {a₀ b₀ : ℝ},
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → IntervalIntegrable (F x) μ a₀ b₀
⊢ IntervalIntegrable (F x) μ b₀ t

Tactic:
exact hiF hx hb₀ ht

Result:
no goals

Proof state:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
⊢ ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)

Tactic:
have Icc_nhds : Icc a b ∈ 𝓝 b₀ := Icc_mem_nhds hb₀.1 hb₀.2

Result:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
⊢ ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)

Proof state:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
⊢ ∀ᶠ (p : X × ℝ) in 𝓝 x₀ ×ˢ 𝓝 b₀,
    ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ =
      ∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ + ∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ

Tactic:
refine (h_bound.prod_mk Ioo_nhds).mono ?_

Result:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x => F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
⊢ ∀ (x : X × ℝ),
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x.1 t‖ ≤ bound t) ∧ a < x.2 ∧ x.2 < b →
      ∫ (s : ℝ) in a₀..x.2, F x.1 s ∂μ =
        ∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ