awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
refine_2 :
  ∀ (hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm.{u_1, u_5} (ε := G) (fun (x : α) ↦ F i x - f x) 1 μ) l (𝓝 0)),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm.{u_1, u_5} (ε := G) (fun (x : α) ↦ F i x - f x) 1 (μ.restrict s)) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α) in s, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
simp_rw [← eLpNorm_one_eq_lintegral_enorm] at hF ⊢

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
s : Set α
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm.{u_1, u_5} (ε := G) (fun (x : α) ↦ F i x - f x) 1 μ) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm.{u_1, u_5} (ε := G) (fun (x : α) ↦ F i x - f x) 1 (μ.restrict s)) l (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hF (fun _ ↦ zero_le)
      (fun _ ↦ eLpNorm_mono_measure _ Measure.restrict_le_self)

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, HSub.hSub, MeasureTheory.Measure.restrict_le_self, MeasureTheory.eLpNorm_mono_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
s : Set α
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm.{u_1, u_5} (ε := G) (fun (x : α) ↦ F i x - f x) 1 μ) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm.{u_1, u_5} (ε := G) (fun (x : α) ↦ F i x - f x) 1 (μ.restrict s)) l (𝓝 0)

Tactic:
exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hF (fun _ ↦ zero_le)
      (fun _ ↦ eLpNorm_mono_measure _ Measure.restrict_le_self)

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, HSub.hSub, MeasureTheory.Measure.restrict_le_self, MeasureTheory.eLpNorm_mono_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)
s : Set α
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))

Tactic:
tendsto_setIntegral_of_L1 f hfi hFi ?_ s

Premises used: MeasureTheory.tendsto_setIntegral_of_L1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)
s : Set α
refine : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))

Tactic:
refine tendsto_setIntegral_of_L1 f hfi hFi ?_ s

Premises used: MeasureTheory.tendsto_setIntegral_of_L1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)
s : Set α
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
s : Set α
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
hF
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
s : Set α
hF : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
exact hF
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : 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.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) s x₀
simp : ContinuousWithinAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) s x₀
⊢ ContinuousWithinAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ ∫ (a : α), F x a ∂μ) s x₀

Tactic:
simp only [integral_eq_setToFun]

Premises used: MeasureTheory.integral_eq_setToFun
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : 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.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) s x₀
⊢ ContinuousWithinAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) s x₀

Tactic:
continuousWithinAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
    hF_meas h_bound bound_integrable h_cont

Premises used: MeasureTheory.dominatedFinMeasAdditive_weightedSMul, MeasureTheory.continuousWithinAt_setToFun_of_dominated
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : 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.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) s x₀
⊢ ContinuousWithinAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) s x₀

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

Premises used: MeasureTheory.dominatedFinMeasAdditive_weightedSMul, MeasureTheory.continuousWithinAt_setToFun_of_dominated
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) x₀
simp : ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) x₀
⊢ ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ ∫ (a : α), F x a ∂μ) x₀

Tactic:
simp only [integral_eq_setToFun]

Premises used: MeasureTheory.integral_eq_setToFun
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) x₀
⊢ ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) x₀

Tactic:
continuousAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
    hF_meas h_bound bound_integrable h_cont

Premises used: MeasureTheory.continuousAt_setToFun_of_dominated, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) x₀
⊢ ContinuousAt.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) x₀

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

Premises used: MeasureTheory.continuousAt_setToFun_of_dominated, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
s : Set X
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) s
simp : ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) s
⊢ ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ ∫ (a : α), F x a ∂μ) s

Tactic:
simp only [integral_eq_setToFun]

Premises used: MeasureTheory.integral_eq_setToFun
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
s : Set X
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) s
⊢ ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) s

Tactic:
continuousOn_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
    hF_meas h_bound bound_integrable h_cont

Premises used: MeasureTheory.continuousOn_setToFun_of_dominated, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
s : Set X
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ F x a) s
⊢ ContinuousOn.{u_6, u_5} (Y := G) (fun (x : X) ↦ setToFun μ (weightedSMul μ) ⋯ (F x)) s

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

Premises used: MeasureTheory.continuousOn_setToFun_of_dominated, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) μ
h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ F x a
simp :
  Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    setToFun μ (weightedSMul μ) ⋯ (F x)
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ ∫ (a : α), F x a ∂μ

Tactic:
simp only [integral_eq_setToFun]

Premises used: MeasureTheory.integral_eq_setToFun
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) μ
h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ F x a
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    setToFun μ (weightedSMul μ) ⋯ (F x)

Tactic:
continuous_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
    hF_meas h_bound bound_integrable h_cont

Premises used: MeasureTheory.continuous_setToFun_of_dominated, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → α → G
bound : α → ℝ
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) μ
h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ F x a
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    setToFun μ (weightedSMul μ) ⋯ (F x)

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

Premises used: MeasureTheory.continuous_setToFun_of_dominated, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
rw :
  (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = (∫⁻ (a : α), ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖

Tactic:
rw [L1.norm_def]

Premises used: MeasureTheory.L1.norm_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
e_a : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = (∫⁻ (a : α), ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ).toReal

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
e_a :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) fun (a : α) ↦
    ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
h :
  ∀ (a : α) (h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0)
    (h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a),
    ENNReal.ofReal (f a) = ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) fun (a : α) ↦
    ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ

Tactic:
filter_upwards [Lp.coeFn_posPart f₁, hf.coeFn_toL1] with _ h₁ h₂

Premises used: MeasureTheory.Integrable.coeFn_toL1, MeasureTheory.Lp.coeFn_posPart
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
h : (↑(f a).toNNReal : ℝ≥0∞) = ‖max (f a) 0‖ₑ
⊢ ENNReal.ofReal (f a) = ‖(↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ

Tactic:
rw [h₁, h₂, ENNReal.ofReal]

Premises used: ENNReal.ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
h : (f a).toNNReal = ‖max (f a) 0‖₊
⊢ (↑(f a).toNNReal : ℝ≥0∞) = ‖max (f a) 0‖ₑ

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
h : (↑(f a).toNNReal : ℝ) = (↑‖max (f a) 0‖₊ : ℝ)
⊢ (f a).toNNReal = ‖max (f a) 0‖₊

Tactic:
apply NNReal.eq

Premises used: NNReal.eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
h : (↑(f a).toNNReal : ℝ) = (↑(NNReal.mk (max (f a) 0) ⋯) : ℝ)
⊢ (↑(f a).toNNReal : ℝ) = (↑‖max (f a) 0‖₊ : ℝ)

Tactic:
rw [Real.nnnorm_of_nonneg (le_max_right _ _)]

Premises used: le_max_right, Real.nnnorm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a : α
h₁ : (↑(↑(Lp.posPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = max ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
h : max (f a) 0 = (↑(NNReal.mk (max (f a) 0) ⋯) : ℝ)
h₃ h₄ : max (f a) 0 = max (f a) 0
⊢ (↑(f a).toNNReal : ℝ) = (↑(NNReal.mk (max (f a) 0) ⋯) : ℝ)

Tactic:
rw [Real.coe_toNNReal', NNReal.coe_mk]

Premises used: Real.coe_toNNReal', NNReal.coe_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖

Tactic:
have eq₁ : ENNReal.toReal (∫⁻ a, ENNReal.ofReal (f a) ∂μ) = ‖Lp.posPart f₁‖ := by
    rw [L1.norm_def]
    congr 1
    apply lintegral_congr_ae
    filter_upwards [Lp.coeFn_posPart f₁, hf.coeFn_toL1] with _ h₁ h₂
    rw [h₁, h₂, ENNReal.ofReal]
    congr 1
    apply NNReal.eq
    rw [Real.nnnorm_of_nonneg (le_max_right _ _)]
    rw [Real.coe_toNNReal', NNReal.coe_mk]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
rw :
  (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = (∫⁻ (a : α), ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖

Tactic:
rw [L1.norm_def]

Premises used: MeasureTheory.L1.norm_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
e_a : ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = ∫⁻ (a : α), ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = (∫⁻ (a : α), ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ).toReal

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
e_a :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) fun (a : α) ↦
    ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
⊢ ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = ∫⁻ (a : α), ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
h :
  ∀ (a : α) (h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0)
    (h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a),
    ENNReal.ofReal (-f a) = ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) fun (a : α) ↦
    ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ

Tactic:
filter_upwards [Lp.coeFn_negPart f₁, hf.coeFn_toL1] with _ h₁ h₂

Premises used: MeasureTheory.Integrable.coeFn_toL1, MeasureTheory.Lp.coeFn_negPart
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a : α
h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
h : (↑(-f a).toNNReal : ℝ≥0∞) = ‖-min (f a) 0‖ₑ
⊢ ENNReal.ofReal (-f a) = ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ

Tactic:
rw [h₁, h₂, ENNReal.ofReal]

Premises used: ENNReal.ofReal