-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem continuousWithinAt_of_dominated {F : X → α → G} {x₀ : X} {bound : α → ℝ} {s : Set X}
    (hF_meas : ∀ᶠ x in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ)
    (h_bound : ∀ᶠ x in 𝓝[s] x₀, ∀ᵐ a ∂μ, ‖F x a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
    (h_cont : ∀ᵐ a ∂μ, ContinuousWithinAt (fun x => F x a) s x₀) :
    ContinuousWithinAt (fun x => ∫ a, F x a ∂μ) s x₀

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => F x a) s x₀
hG : CompleteSpace G
⊢ ContinuousWithinAt
    (fun x =>
      if h : True then
        if hf : Integrable (fun a => F x a) μ then L1.integralCLM (Integrable.toL1 (fun a => F x a) hf) else 0
      else 0)
    s x₀

Tactic:
exact continuousWithinAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
  hF_meas h_bound bound_integrable h_cont

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => F x a) s x₀
hG : ¬CompleteSpace G
⊢ ContinuousWithinAt (fun x => ∫ (a : α), F x a ∂μ) s x₀

Tactic:
simp [integral, hG, continuousWithinAt_const]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => F x a) s x₀
⊢ ContinuousWithinAt (fun x => ∫ (a : α), F x a ∂μ) s x₀

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => F x a) s x₀
hG : CompleteSpace G
⊢ ContinuousWithinAt (fun x => ∫ (a : α), F x a ∂μ) s x₀

case neg
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => F x a) s x₀
hG : ¬CompleteSpace G
⊢ ContinuousWithinAt (fun x => ∫ (a : α), F x a ∂μ) s x₀

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => F x a) s x₀
hG : CompleteSpace G
⊢ ContinuousWithinAt (fun x => ∫ (a : α), F x a ∂μ) s x₀

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => F x a) s x₀
hG : CompleteSpace G
⊢ ContinuousWithinAt
    (fun x =>
      if h : True then
        if hf : Integrable (fun a => F x a) μ then L1.integralCLM (Integrable.toL1 (fun a => F x a) hf) else 0
      else 0)
    s x₀