awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
hF_meas : ∀ (a : X), Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ AEStronglyMeasurable (f x) (μ.restrict s)) x} a
hF_meas₁ hF_meas₂ : ∀ (x : X), AEStronglyMeasurable (f x) (μ.restrict s)
⊢ ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (f x) (μ.restrict s)

Tactic:
filter_upwards with x using Continuous.aestronglyMeasurable (by fun_prop)

Premises used: Continuous.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
h : ∀ (x : X) (x_in : x ∈ U), ∀ᵐ (a : Y) ∂μ.restrict s, ‖f x a‖ ≤ M
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : Y) ∂μ.restrict s, ‖f x a‖ ≤ M

Tactic:
filter_upwards [U_nhds] with x x_in
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
x : X
x_in : x ∈ U
h : ∀ᵐ (x_1 : Y) ∂μ, x_1 ∈ s → ‖f x x_1‖ ≤ M
h₁ : MeasurableSet.{u_2} (α := Y) {x_1 : Y | ‖f x x_1‖ ≤ M}
⊢ ∀ᵐ (a : Y) ∂μ.restrict s, ‖f x a‖ ≤ M

Tactic:
rw [ae_restrict_iff]

Premises used: MeasureTheory.ae_restrict_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
x : X
x_in : x ∈ U
t : Y
t_in : t ∈ s
⊢ ‖f x t‖ ≤ M

Tactic:
hM (mem_image_of_mem _ <| mk_mem_prod x_in t_in)

Premises used: Set.mem_image_of_mem, Set.mk_mem_prod
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
x : X
x_in : x ∈ U
h : ∀ (a : Y), Membership.mem (γ := Set Y) {x_1 : Y | (fun (x_2 : Y) ↦ x_2 ∈ s → ‖f x x_2‖ ≤ M) x_1} a
h₁ h₂ : ∀ (t : Y) (t_in : t ∈ s), ‖f x t‖ ≤ M
⊢ ∀ᵐ (x_1 : Y) ∂μ, x_1 ∈ s → ‖f x x_1‖ ≤ M

Tactic:
filter_upwards with t t_in using hM (mem_image_of_mem _ <| mk_mem_prod x_in t_in)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
x : X
x_in : x ∈ U
⊢ Continuous[inst_1, _] fun (x_1 : Y) ↦ ‖f x x_1‖

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
x : X
x_in : x ∈ U
⊢ Continuous[inst_1, _] fun (x : Y) ↦ M

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
x : X
x_in : x ∈ U
⊢ MeasurableSet.{u_2} (α := Y) {x_1 : Y | ‖f x x_1‖ ≤ M}

Tactic:
exact (isClosed_le (by fun_prop) (by fun_prop)).measurableSet

Premises used: isClosed_le, IsClosed.measurableSet
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
⊢ Integrable (ε := ℝ) (fun (t : Y) ↦ M) (μ.restrict s)

Tactic:
integrableOn_const hs.measure_ne_top

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.integrableOn_const, IsCompact.measure_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
⊢ Integrable (ε := ℝ) (fun (t : Y) ↦ M) (μ.restrict s)

Tactic:
exact integrableOn_const hs.measure_ne_top

Premises used: MeasureTheory.integrableOn_const, IsCompact.measure_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
⊢ ∀ (a : Y), ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ f x a) x₀

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
X : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
inst_6 : FirstCountableTopology X
inst_7 : LocallyCompactSpace X
inst_8 : SecondCountableTopologyEither Y E
inst_9 : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M
h_cont :
  ∀ (a : Y),
    Membership.mem (γ := Set Y) {x : Y | (fun (a : Y) ↦ ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ f x a) x₀) x} a
h_cont₁ : ∀ (a : Y), ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ f x a) x₀
⊢ ∀ᵐ (a : Y) ∂μ.restrict s, ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ f x a) x₀

Tactic:
filter_upwards using (by fun_prop)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
p : X
hp : p ∈ s
⊢ Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)

Tactic:
hf.comp_continuous (.prodMk_right _) fun y => ?_

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
p : X
hp : p ∈ s
refine : ∀ (y : Y), (p, y) ∈ SProd.sprod (β := Set Y) s univ
⊢ Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)

Tactic:
refine hf.comp_continuous (.prodMk_right _) fun y => ?_

Premises used: ContinuousOn.comp_continuous, Continuous.prodMk_right
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
p : X
hp : p ∈ s
y : Y
⊢ (p, y) ∈ SProd.sprod (β := Set Y) s univ

Tactic:
simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hp

Premises used: and_true, Set.prodMk_mem_set_prod_eq, Set.mem_univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
⊢ ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)

Tactic:
have A : ∀ p ∈ s, Continuous (f p) := fun p hp ↦ by
    refine hf.comp_continuous (.prodMk_right _) fun y => ?_
    simpa only [prodMk_mem_set_prod_eq, mem_univ, and_true] using hp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
apply :
  ∀ (ε : ℝ) (εpos : ε > 0),
    ∀ᶠ (x : X) in 𝓝[s] q,
      dist.{u_3} (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f x y) ∂μ)
          (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ) <
        ε
⊢ ContinuousWithinAt.{u_5, u_3} (Y := E)
    (fun (x : X) ↦ ∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f x y) ∂μ) s q

Tactic:
apply Metric.continuousWithinAt_iff'.2 (fun ε εpos ↦ ?_)

Premises used: Iff.mpr, Metric.continuousWithinAt_iff'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε

Tactic:
simpa [integral_mul_const] using exists_pos_mul_lt εpos _

Premises used: exists_pos_mul_lt, MeasureTheory.integral_mul_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
obtain :
  ∀ (δ : ℝ) (δpos : 0 < δ) (hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε),
    ∀ᶠ (x : X) in 𝓝[s] q,
      dist.{u_3} (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f x y) ∂μ)
          (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ) <
        ε
⊢ ∀ᶠ (x : X) in 𝓝[s] q,
    dist.{u_3} (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f x y) ∂μ)
        (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ) <
      ε

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ (δ : ℝ), 0 < δ ∧ ∫ x in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε := by
    simpa [integral_mul_const] using exists_pos_mul_lt εpos _
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, dist (f p x) (f q x) < δ

Tactic:
hk.mem_uniformity_of_prod
      (hf.mono (Set.prod_mono_right (subset_univ k))) hq (dist_mem_uniformity δpos)

Premises used: IsCompact.mem_uniformity_of_prod, Set.prod_mono_right, Set.Mem, Set.subset_univ, ContinuousOn.mono, Metric.dist_mem_uniformity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
obtain :
  ∀ (v : Set X) (v_mem : v ∈ 𝓝[s] q) (hv : ∀ p ∈ v, ∀ x ∈ k, dist (f p x) (f q x) < δ),
    ∀ᶠ (x : X) in 𝓝[s] q,
      dist.{u_3} (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f x y) ∂μ)
          (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ) <
        ε
⊢ ∀ᶠ (x : X) in 𝓝[s] q,
    dist.{u_3} (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f x y) ∂μ)
        (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ) <
      ε

Tactic:
obtain ⟨v, v_mem, hv⟩ : ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, dist (f p x) (f q x) < δ :=
    hk.mem_uniformity_of_prod
      (hf.mono (Set.prod_mono_right (subset_univ k))) hq (dist_mem_uniformity δpos)

Premises used: IsCompact.mem_uniformity_of_prod, Set.prod_mono_right, Set.subset_univ, ContinuousOn.mono, Metric.dist_mem_uniformity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : MeasurableSpace Y
inst_3 : OpensMeasurableSpace Y
μ : Measure Y
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℝ E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : NormedAddCommGroup G
inst_10 : NormedSpace 𝕜 G
inst_11 : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (SProd.sprod (β := Set Y) s univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
v : Set X
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ k, dist (f p x) (f q x) < δ
simp_rw :
  ∀ (hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ),
    ∀ᶠ (x : X) in 𝓝[s] q,
      ‖HSub.hSub (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f x y) ∂μ)
            (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ)‖ <
        ε
⊢ ∀ᶠ (x : X) in 𝓝[s] q,
    dist.{u_3} (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f x y) ∂μ)
        (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ) <
      ε

Tactic:
simp_rw [dist_eq_norm] at hv ⊢

Premises used: dist_eq_norm