-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem continuousOn_setToFun_of_dominated (hT : DominatedFinMeasAdditive μ T C) {fs : X → α → E}
    {bound : α → ℝ} {s : Set X} (hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ)
    (h_bound : ∀ x ∈ s, ∀ᵐ a ∂μ, ‖fs x a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
    (h_cont : ∀ᵐ a ∂μ, ContinuousOn (fun x => fs x a) s) :
    ContinuousOn (fun x => setToFun μ T hT (fs x)) s

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
⊢ ContinuousOn (fun x => setToFun μ T hT (fs x)) s

Tactic:
intro x hx

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ContinuousWithinAt (fun x => setToFun μ T hT (fs x)) s x

Proof state:
case refine_2
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx using h_bound x hx

Result:
no goals

Proof state:
case refine_3
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => fs x a) s x

Tactic:
filter_upwards [h_cont] with a ha using ha x hx

Result:
no goals

Proof state:
case refine_1
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx using hfs_meas x hx

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ContinuousWithinAt (fun x => setToFun μ T hT (fs x)) s x

Tactic:
refine continuousWithinAt_setToFun_of_dominated hT ?_ ?_ bound_integrable ?_

Result:
case refine_1
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ

case refine_2
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a

case refine_3
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => fs x a) s x