awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
⊢ Eq (α := (f : ↥(Lp E 1 μ)) → E) (fun (f : ↥(Lp E 1 μ)) ↦ ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))

Tactic:
have h_comp :
    (fun f : X →₁[μ] E => ∫ x in s, f x ∂μ) =
      integral (μ.restrict s) ∘ fun f => LpToLpRestrictCLM X E ℝ μ 1 s f := by
    ext1 f
    rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
h_comp :
  Eq (α := (f : ↥(Lp E 1 μ)) → E) (fun (f : ↥(Lp E 1 μ)) ↦ ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))
rw :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp E 1 μ)) ↦
    ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ

Tactic:
rw [h_comp]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
h_comp :
  Eq (α := (f : ↥(Lp E 1 μ)) → E) (fun (f : ↥(Lp E 1 μ)) ↦ ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))

Tactic:
continuous_integral.comp (LpToLpRestrictCLM X E ℝ μ 1 s).continuous

Premises used: Real, MeasureTheory.LpToLpRestrictCLM, Continuous.comp, ContinuousLinearMap.continuous, MeasureTheory.continuous_integral, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
inst_1 : NormedSpace ℝ E
s : Set X
this : Fact (LE.le (α := ℝ≥0∞) 1 1)
h_comp :
  Eq (α := (f : ↥(Lp E 1 μ)) → E) (fun (f : ↥(Lp E 1 μ)) ↦ ∫ (x : X) in s, (↑(↑f : X →ₘ[μ] E) : X → E) x ∂μ)
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (integral (μ.restrict s) ∘ fun (f : ↥(Lp E 1 μ)) ↦
      (↑(↑((LpToLpRestrictCLM X E ℝ μ 1 s : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 (μ.restrict s))) f) : X →ₘ[μ.restrict s] E) :
        X → E))

Tactic:
exact continuous_integral.comp (LpToLpRestrictCLM X E ℝ μ 1 s).continuous

Premises used: Real, MeasureTheory.LpToLpRestrictCLM, Continuous.comp, ContinuousLinearMap.continuous, MeasureTheory.continuous_integral, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
inst_4 : IsFiniteMeasureOnCompacts μ
f : X → ℝ
x : X
f_cont : Continuous[inst_1, _] f
f_comp : HasCompactSupport f
f_nonneg : 0 ≤ f
f_x : f x ≠ 0
⊢ LT.lt (α := ℝ) 0 (∫ (x : X), f x ∂μ)

Tactic:
integral_pos_of_integrable_nonneg_nonzero f_cont (f_cont.integrable_of_hasCompactSupport f_comp)
    f_nonneg f_x

Premises used: Continuous.integrable_of_hasCompactSupport, MeasureTheory.integral_pos_of_integrable_nonneg_nonzero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
nth_rw : Eq.{u_5 + 1} (α := M) (∫ (x : X) in support F, F x ∂ν) (∫ (x : X) in univ, F x ∂ν)
⊢ Eq.{u_5 + 1} (α := M) (∫ (x : X) in support F, F x ∂ν) (∫ (x : X), F x ∂ν)

Tactic:
nth_rw 2 [← setIntegral_univ]

Premises used: MeasureTheory.setIntegral_univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
rw : ∀ x ∈ univ \ support F, F x = 0
⊢ Eq.{u_5 + 1} (α := M) (∫ (x : X) in support F, F x ∂ν) (∫ (x : X) in univ, F x ∂ν)

Tactic:
rw [setIntegral_eq_of_subset_of_forall_diff_eq_zero MeasurableSet.univ (subset_univ (support F))]

Premises used: Set.subset_univ, Function.support, MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
⊢ ∀ x ∈ univ \ support F, F x = 0

Tactic:
fun _ hx => notMem_support.mp <| notMem_of_mem_diff hx

Premises used: Function.notMem_support, Set.notMem_of_mem_diff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
⊢ ∀ x ∈ univ \ support F, F x = 0

Tactic:
exact fun _ hx => notMem_support.mp <| notMem_of_mem_diff hx

Premises used: Function.notMem_support, Set.notMem_of_mem_diff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst_2 : TopologicalSpace X
nth_rw : Eq.{u_5 + 1} (α := M) (∫ (x : X) in tsupport F, F x ∂ν) (∫ (x : X) in univ, F x ∂ν)
⊢ Eq.{u_5 + 1} (α := M) (∫ (x : X) in tsupport F, F x ∂ν) (∫ (x : X), F x ∂ν)

Tactic:
nth_rw 2 [← setIntegral_univ]

Premises used: MeasureTheory.setIntegral_univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst_2 : TopologicalSpace X
rw : ∀ x ∈ univ \ tsupport F, F x = 0
⊢ Eq.{u_5 + 1} (α := M) (∫ (x : X) in tsupport F, F x ∂ν) (∫ (x : X) in univ, F x ∂ν)

Tactic:
rw [setIntegral_eq_of_subset_of_forall_diff_eq_zero MeasurableSet.univ (subset_univ (tsupport F))]

Premises used: Set.subset_univ, tsupport, MeasureTheory.setIntegral_eq_of_subset_of_forall_diff_eq_zero, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst_2 : TopologicalSpace X
⊢ ∀ x ∈ univ \ tsupport F, F x = 0

Tactic:
fun _ hx => image_eq_zero_of_notMem_tsupport <| notMem_of_mem_diff hx

Premises used: image_eq_zero_of_notMem_tsupport, Set.notMem_of_mem_diff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
M : Type u_5
inst : NormedAddCommGroup M
inst_1 : NormedSpace ℝ M
mX : MeasurableSpace X
ν : Measure X
F : X → M
inst_2 : TopologicalSpace X
⊢ ∀ x ∈ univ \ tsupport F, F x = 0

Tactic:
exact fun _ hx => image_eq_zero_of_notMem_tsupport <| notMem_of_mem_diff hx

Premises used: image_eq_zero_of_notMem_tsupport, Set.notMem_of_mem_diff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
h : (μ : (a : Set X) → ℝ≥0∞) E = lintegral μ (E.indicator fun (x : X) ↦ 1)
convert_to : lintegral μ (E.indicator fun (x : X) ↦ 1) ≤ lintegral μ (thickenedIndicatorAux δ E)
⊢ (μ : (a : Set X) → ℝ≥0∞) E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ

Tactic:
convert_to lintegral μ (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ lintegral μ (thickenedIndicatorAux δ E)

Premises used: Set.indicator, thickenedIndicatorAux, OfNat.ofNat, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
h : (μ : (a : Set X) → ℝ≥0∞) E = ∫⁻ (a : X) in E, 1 ∂μ
⊢ (μ : (a : Set X) → ℝ≥0∞) E = lintegral μ (E.indicator fun (x : X) ↦ 1)

Tactic:
rw [lintegral_indicator E_mble]

Premises used: MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ (μ : (a : Set X) → ℝ≥0∞) E = ∫⁻ (a : X) in E, 1 ∂μ

Tactic:
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ, MeasureTheory.lintegral_one
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
hfg : (E.indicator fun (x : X) ↦ 1) ≤ thickenedIndicatorAux δ E
⊢ lintegral μ (E.indicator fun (x : X) ↦ 1) ≤ lintegral μ (thickenedIndicatorAux δ E)

Tactic:
apply lintegral_mono

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ (E.indicator fun (x : X) ↦ 1) ≤ thickenedIndicatorAux δ E

Tactic:
apply indicator_le_thickenedIndicatorAux

Premises used: indicator_le_thickenedIndicatorAux
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
⊢ (μ : (a : Set X) → ℝ≥0∞) E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ

Tactic:
measure_le_lintegral_thickenedIndicatorAux μ E_mble δ

Premises used: measure_le_lintegral_thickenedIndicatorAux
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
h :
  ∀ (x : X),
    (↑(((thickenedIndicator δ_pos E : BoundedContinuousFunction X ℝ≥0) : (a : X) → ℝ≥0) x) : ℝ≥0∞) =
      thickenedIndicatorAux δ E x
⊢ (μ : (a : Set X) → ℝ≥0∞) E ≤
    ∫⁻ (x : X), (↑(((thickenedIndicator δ_pos E : BoundedContinuousFunction X ℝ≥0) : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ

Tactic:
convert! measure_le_lintegral_thickenedIndicatorAux μ E_mble δ

Premises used: measure_le_lintegral_thickenedIndicatorAux
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
δ_pos : 0 < δ
x : X
⊢ (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ≥0∞) = thickenedIndicatorAux δ E x

Tactic:
simp only [thickenedIndicatorAux_lt_top.ne, ENNReal.coe_toNNReal, Ne, not_false_iff]

Premises used: ENNReal.coe_toNNReal, thickenedIndicatorAux_lt_top, Ne, not_false_iff, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
g₁ g₂ : SimpleFunc X ℝ
h : Disjoint (α := Set X) (support (M := ℝ) (⇑g₁ : (a : X) → ℝ)) (support (M := ℝ) (⇑g₂ : (a : X) → ℝ))
h_int₁ : Integrable ((⇑g₁ : (a : X) → ℝ) * f) μ
h_int₂ : Integrable ((⇑g₂ : (a : X) → ℝ) * f) μ
rw :
  (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f =ᶠ[ae μ]
    HAdd.hAdd (α := (a : X) → ℝ) (⇑g₁ : (a : X) → ℝ) (⇑g₂ : (a : X) → ℝ) * f
rw₁ rw₂ : (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f =ᶠ[ae μ] (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f
⊢ (⇑g₁ : (a : X) → ℝ) * f + (⇑g₂ : (a : X) → ℝ) * f =ᶠ[ae μ] (⇑(g₁ + g₂) : (a : X) → ℝ) * f

Tactic:
rw [SimpleFunc.coe_add, add_mul]

Premises used: add_mul, MeasureTheory.SimpleFunc.coe_add
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c :
  ∀ (c : ℝ) (s : Set X) (hs : MeasurableSet s),
    Integrable ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const X c) (SimpleFunc.const X 0)) : (a : X) → ℝ) * f) μ
⊢ Integrable ((⇑g : (a : X) → ℝ) * f) μ

Tactic:
refine
    SimpleFunc.induction (fun c s hs => ?_)
      (fun g₁ g₂ _ h_int₁ h_int₂ =>
        (h_int₁.add h_int₂).congr (by rw [SimpleFunc.coe_add, add_mul]))
      g
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
simp : Integrable (s.indicator (const X c) * f) μ
⊢ Integrable ((⇑(SimpleFunc.piecewise s hs (SimpleFunc.const X c) (SimpleFunc.const X 0)) : (a : X) → ℝ) * f) μ

Tactic:
simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const,
    SimpleFunc.coe_zero, Set.piecewise_eq_indicator]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, MeasureTheory.SimpleFunc.coe_zero, MeasureTheory.SimpleFunc.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
h : ∀ (x : X), (s.indicator (const X c) * f) x = s.indicator (c • f) x
⊢ s.indicator (const X c) * f = s.indicator (c • f)

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
pos : ∀ (hx : x ∈ s), (s.indicator (const X c) * f) x = s.indicator (c • f) x
neg : ∀ (hx : x ∉ s), (s.indicator (const X c) * f) x = s.indicator (c • f) x
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∈ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Tactic:
simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, smul_eq_mul,
        ← Function.const_def]

Premises used: Pi.mul_apply, Set.indicator_of_mem, Function.const_def, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∉ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Tactic:
simp only [hx, Pi.mul_apply, Set.indicator_of_notMem, not_false_iff, zero_mul]

Premises used: Pi.mul_apply, MulZeroClass.zero_mul, Set.indicator_of_notMem, not_false_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
⊢ s.indicator (const X c) * f = s.indicator (c • f)

Tactic:
have : Set.indicator s (Function.const X c) * f = s.indicator (c • f) := by
    ext1 x
    by_cases hx : x ∈ s
    · simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, smul_eq_mul,
        ← Function.const_def]
    · simp only [hx, Pi.mul_apply, Set.indicator_of_notMem, not_false_iff, zero_mul]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
this : s.indicator (const X c) * f = s.indicator (c • f)
rw : IntegrableOn (c • f) s μ
⊢ Integrable (s.indicator (const X c) * f) μ

Tactic:
rw [this, integrable_indicator_iff hs]

Premises used: MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
this : s.indicator (const X c) * f = s.indicator (c • f)
⊢ IntegrableOn (c • f) s μ

Tactic:
(hf.smul c).integrableOn

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
this : s.indicator (const X c) * f = s.indicator (c • f)
⊢ IntegrableOn (c • f) s μ

Tactic:
exact (hf.smul c).integrableOn

Premises used: MeasureTheory.Integrable.smul, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
g : SimpleFunc X ℝ
hf : Integrable f μ
rw : Integrable ((⇑(SimpleFunc.toLargerSpace hm g) : (a : X) → ℝ) * f) μ
⊢ Integrable ((⇑g : (a : X) → ℝ) * f) μ

Tactic:
rw [← SimpleFunc.coe_toLargerSpace_eq hm g]

Premises used: MeasureTheory.SimpleFunc.coe_toLargerSpace_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable ((⇑(SimpleFunc.toLargerSpace hm g) : (a : X) → ℝ) * f) μ

Tactic:
hf.simpleFunc_mul (g.toLargerSpace hm)

Premises used: MeasureTheory.Integrable.simpleFunc_mul, MeasureTheory.SimpleFunc.toLargerSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_6
f : X → ℝ
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
g : SimpleFunc X ℝ
hf : Integrable f μ
⊢ Integrable ((⇑(SimpleFunc.toLargerSpace hm g) : (a : X) → ℝ) * f) μ

Tactic:
exact hf.simpleFunc_mul (g.toLargerSpace hm)

Premises used: MeasureTheory.Integrable.simpleFunc_mul, MeasureTheory.SimpleFunc.toLargerSpace
-- 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
rw : ∀ (x : X), ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ ∫ (y : Y) in s, f x y ∂μ) x
⊢ Continuous[inst, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ ∫ (y : Y) in s, f x y ∂μ

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- 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
rcases :
  ∀ (U : Set X) (U_cpct : IsCompact U) (U_nhds : U ∈ 𝓝 x₀),
    ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ ∫ (y : Y) in s, f x y ∂μ) x₀
⊢ ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ ∫ (y : Y) in s, f x y ∂μ) x₀

Tactic:
rcases exists_compact_mem_nhds x₀ with ⟨U, U_cpct, U_nhds⟩

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- 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₀
rcases :
  ∀ (M : ℝ) (hM : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : X × Y) ↦ ‖uncurry f x‖) '' U ×ˢ s)) M),
    ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ ∫ (y : Y) in s, f x y ∂μ) x₀
⊢ ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ ∫ (y : Y) in s, f x y ∂μ) x₀

Tactic:
rcases (U_cpct.prod hs).bddAbove_image hf.norm.continuousOn with ⟨M, hM⟩

Premises used: Continuous.continuousOn, IsCompact.prod, Continuous.norm, IsCompact.bddAbove_image
-- 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 : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (f x) (μ.restrict s)
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : Y) ∂μ.restrict s, ‖f x a‖ ≤ M
bound_integrable : Integrable (ε := ℝ) (fun (t : Y) ↦ M) (μ.restrict s)
h_cont : ∀ᵐ (a : Y) ∂μ.restrict s, ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ f x a) x₀
bound : Y → ℝ
⊢ ContinuousAt.{u_5, u_3} (Y := E) (fun (x : X) ↦ ∫ (y : Y) in s, f x y ∂μ) x₀

Tactic:
apply continuousAt_of_dominated

Premises used: MeasureTheory.continuousAt_of_dominated
-- 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
⊢ Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f x)

Tactic:
fun_prop