awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
p : X
hp : p ∈ s
C : ℝ
hC : ∀ (y : Y), ‖f p y‖ ≤ C
this : IntegrableOn (ε := ℝ) (fun (y : Y) ↦ ‖L‖ * ‖g y‖ * C) k μ
y : Y
⊢ ‖L‖ * ‖g y‖ * ‖f p y‖ ≤ ‖L‖ * ‖g y‖ * C
have hbc : ‖f p y‖ ≤ C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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, ‖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) ∂μ)‖ <
      ε
have I : ∀ p ∈ s,
  IntegrableOn.{u_2, u_3} (ε := E) (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y))
    k μ
Tactic: have I : ∀ p ∈ s, IntegrableOn (fun y ↦ L (g y) (f p y)) k μ := by
    intro p hp
    obtain ⟨C, hC⟩ : ∃ C, ∀ y, ‖f p y‖ ≤ C := by
      have : ContinuousOn (f p) k := by
        have : ContinuousOn (fun y ↦ (p, y)) k := by fun_prop
        exact hf.comp this (by simp [MapsTo, hp])
      rcases IsCompact.exists_bound_of_continuousOn hk this with ⟨C, hC⟩
      refine ⟨max C 0, fun y ↦ ?_⟩
      by_cases hx : y ∈ k
      · exact (hC y hx).trans (le_max_left _ _)
      · simp [hfs p y hp hx]
    have : IntegrableOn (fun y ↦ ‖L‖ * ‖g y‖ * C) k μ :=
      (hg.norm.const_mul _).mul_const _
    apply Integrable.mono' this ?_ ?_
    · borelize G
      apply L.aestronglyMeasurable_comp₂ hg.aestronglyMeasurable
      apply StronglyMeasurable.aestronglyMeasurable
      apply Continuous.stronglyMeasurable_of_support_subset_isCompact (A p hp) hk
      apply support_subset_iff'.2 (fun y hy ↦ hfs p y hp hy)
    · apply Eventually.of_forall (fun y ↦ (le_opNorm₂ L (g y) (f p y)).trans ?_)
      gcongr
      apply hC
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
⊢ ∀ᶠ (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) ∂μ)‖ <
      ε
have h : ∀ (p : X) (hp : p ∈ v) (h'p : p ∈ s),
  ‖HSub.hSub (α := E) (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) ∂μ)
        (∫ (y : Y), (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) ∂μ)‖ <
    ε
Tactic: filter_upwards [v_mem, self_mem_nhdsWithin] with p hp h'p
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ ‖HSub.hSub (α := E) (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
        (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖ =
    ‖HSub.hSub (α := E) (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
        (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖
have e_a : Eq.{u_3 + 1} (α := E) (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
  (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
e_a :
  Eq.{u_3 + 1} (α := E) (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
    (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
⊢ ‖HSub.hSub (α := E) (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
        (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖ =
    ‖HSub.hSub (α := E) (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
        (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖
have e_a₁ : Eq.{u_3 + 1} (α := E) (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)
  (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
    (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
have e_a : ∀ (y : Y) (hy : y ∉ k),
  Eq.{u_3 + 1} (α := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E) (0 : E)
Tactic: refine (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : Y), (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)
    (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)
have e_a : ∀ (y : Y) (hy : y ∉ k),
  Eq.{u_3 + 1} (α := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E) (0 : E)
Tactic: refine (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ ‖HSub.hSub (α := E) (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
        (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖ =
    norm.{u_3} (E := E)
      (∫ (x : Y) in k,
        HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) : E) ∂μ)
have rw : ‖HSub.hSub (α := E) (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) ∂μ)
      (∫ (x : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) ∂μ)‖ =
  ‖HSub.hSub (α := E) (∫ (a : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f p a) ∂μ)
      (∫ (a : Y) in k, (((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f q a) ∂μ)‖
Tactic: rw [integral_sub (I p h'p) (I q hq)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ LE.le (α := ℝ)
    (∫ (x : Y) in k,
      ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) : E)‖ ∂μ)
    (∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ)
have hgi : Integrable (ε := ℝ) (fun (a : Y) ↦ ‖L‖ * ‖g a‖ * δ) (μ.restrict k)
Tactic: apply integral_mono_of_nonneg (Eventually.of_forall (fun y ↦ by positivity))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
hgi : Integrable (ε := ℝ) (fun (a : Y) ↦ ‖L‖ * ‖g a‖ * δ) (μ.restrict k)
⊢ LE.le (α := ℝ)
    (∫ (x : Y) in k,
      ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f p x) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g x) : G →L[𝕜] E) : (a : G) → E) (f q x) : E)‖ ∂μ)
    (∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ)
have h : (ae (μ.restrict k)).EventuallyLE (β := ℝ)
  (fun (a : Y) ↦
    ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f p a) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f q a) : E)‖)
  fun (a : Y) ↦ ‖L‖ * ‖g a‖ * δ
Tactic: apply integral_mono_of_nonneg (Eventually.of_forall (fun y ↦ by positivity))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
⊢ (ae (μ.restrict k)).EventuallyLE (β := ℝ)
    (fun (a : Y) ↦
      ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f p a) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g a) : G →L[𝕜] E) : (a : G) → E) (f q a) : E)‖)
    fun (a : Y) ↦ ‖L‖ * ‖g a‖ * δ
have h : ∀ (y : Y),
  ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ
Tactic: filter_upwards with y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ
have pos : ∀ (hy : y ∈ k),
  ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ
Tactic: by_cases hy : y ∈ k
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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, ‖f p x - f q x‖ < δ
I :
  ∀ p ∈ s,
    IntegrableOn.{u_2, u_3} (ε := E)
      (fun (y : Y) ↦ (((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y)) k μ
p : X
hp : p ∈ v
h'p : p ∈ s
y : Y
pos :
  ∀ (hy : y ∈ k),
    ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
          ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
      ‖L‖ * ‖g y‖ * δ
⊢ ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ
have neg : ∀ (hy : y ∉ k),
  ‖HSub.hSub (α := E) (β := E) ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f p y) : E)
        ((((L : (a : F) → G →L[𝕜] E) (g y) : G →L[𝕜] E) : (a : G) → E) (f q y) : E)‖ ≤
    ‖L‖ * ‖g y‖ * δ
Tactic: by_cases hy : y ∈ k