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 α
f g : α → G
h : f =ᶠ[ae μ] g
⊢ setToFun μ (weightedSMul μ) ⋯ f = setToFun μ (weightedSMul μ) ⋯ g

Tactic:
exact setToFun_congr_ae (dominatedFinMeasAdditive_weightedSMul μ) h

Premises used: MeasureTheory.setToFun_congr_ae, 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 α
β : Type u_6
x : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
h₁ : EventuallyEq.{u_1, u_5} (β := G) (ae μ) (fun (a : α) ↦ ∫ (b : β), f a b ∂ν) fun (a : α) ↦ ∫ (b : β), g a b ∂ν
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), ∫ (b : β), f a b ∂ν ∂μ) (∫ (a : α), ∫ (b : β), g a b ∂ν ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- 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
x : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
h₁ : ∀ (a : α) (ha : f a =ᶠ[ae ν] g a), Eq.{u_5 + 1} (α := G) (∫ (b : β), f a b ∂ν) (∫ (b : β), g a b ∂ν)
⊢ EventuallyEq.{u_1, u_5} (β := G) (ae μ) (fun (a : α) ↦ ∫ (b : β), f a b ∂ν) fun (a : α) ↦ ∫ (b : β), g a b ∂ν

Tactic:
filter_upwards [h] with _ ha
-- 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
x : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
a : α
ha h₁ : f a =ᶠ[ae ν] g a
⊢ Eq.{u_5 + 1} (α := G) (∫ (b : β), f a b ∂ν) (∫ (b : β), g a b ∂ν)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- 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
x : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
a : α
ha : f a =ᶠ[ae ν] g a
a_1 : β
hb : f a a_1 = g a a_1
⊢ f a a_1 = g a a_1

Tactic:
hb
-- 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
x : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae ν] g a
a : α
ha : f a =ᶠ[ae ν] g a
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f a x = g a x) x} x}
      a_1
h₂ h₃ : ∀ (a_1 : β) (hb : f a a_1 = g a a_1), f a a_1 = g a a_1
⊢ f a =ᶠ[ae ν] g a

Tactic:
filter_upwards [ha] with _ hb using hb
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
simp : setToFun μ (weightedSMul μ) ⋯ (↑(AEEqFun.mk f ⋯) : α → G) = setToFun μ (weightedSMul μ) ⋯ f
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), (↑(AEEqFun.mk f ⋯) : α → G) a ∂μ) (∫ (a : α), f 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 α
f : α → G
hf : Integrable f μ
⊢ setToFun μ (weightedSMul μ) ⋯ (↑(AEEqFun.mk f ⋯) : α → G) = setToFun μ (weightedSMul μ) ⋯ f

Tactic:
setToFun_toL1 (dominatedFinMeasAdditive_weightedSMul μ) hf

Premises used: MeasureTheory.dominatedFinMeasAdditive_weightedSMul, MeasureTheory.AEEqFun.mk, MeasureTheory.setToFun_toL1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
⊢ setToFun μ (weightedSMul μ) ⋯ (↑(AEEqFun.mk f ⋯) : α → G) = setToFun μ (weightedSMul μ) ⋯ f

Tactic:
exact setToFun_toL1 (dominatedFinMeasAdditive_weightedSMul μ) hf

Premises used: MeasureTheory.dominatedFinMeasAdditive_weightedSMul, MeasureTheory.setToFun_toL1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] G) : α → G) a ∂μ) (∫ (a : α), f a ∂μ)

Tactic:
simp [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 α
simp :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp G 1 μ)) ↦
    setToFun μ (weightedSMul μ) ⋯ (↑(↑f : α →ₘ[μ] G) : α → G)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp G 1 μ)) ↦
    ∫ (a : α), (↑(↑f : α →ₘ[μ] G) : α → G) 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 α
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp G 1 μ)) ↦
    setToFun μ (weightedSMul μ) ⋯ (↑(↑f : α →ₘ[μ] G) : α → G)

Tactic:
continuous_setToFun (dominatedFinMeasAdditive_weightedSMul μ)

Premises used: MeasureTheory.continuous_setToFun, 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 α
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : ↥(Lp G 1 μ)) ↦
    setToFun μ (weightedSMul μ) ⋯ (↑(↑f : α →ₘ[μ] G) : α → G)

Tactic:
exact continuous_setToFun (dominatedFinMeasAdditive_weightedSMul μ)

Premises used: MeasureTheory.continuous_setToFun, 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 α
f : α → G
simp : ‖setToFun μ (weightedSMul μ) ⋯ f‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

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 α
f : α → G
⊢ LE.le (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ (↑(NNReal.mk 1 ⋯) : ℝ) * (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖setToFun μ (weightedSMul μ) ⋯ f‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
exact (norm_setToFun_le_toReal _ (by simp)).trans (by simp)

Premises used: MeasureTheory.norm_setToFun_le_toReal, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
simp : ‖setToFun μ (weightedSMul μ) ⋯ f‖ₑ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
⊢ enorm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫⁻ (a : α), ‖f 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 α
f : α → G
⊢ (↑(NNReal.mk 1 ⋯) : ℝ≥0∞) * ∫⁻ (x : α), ‖f x‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖setToFun μ (weightedSMul μ) ⋯ f‖ₑ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
exact (enorm_setToFun_le _ (by simp)).trans (by simp)

Premises used: MeasureTheory.enorm_setToFun_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
grw : (∫⁻ (a : α), ENNReal.ofReal ‖f a - g a‖ ∂μ).toReal ≤ (∫⁻ (a : α), edist (f a) (g a) ∂μ).toReal
⊢ dist.{u_5} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ≤ (∫⁻ (a : α), edist (f a) (g a) ∂μ).toReal

Tactic:
grw [dist_eq_norm, ← integral_sub hf hg, norm_integral_le_lintegral_norm]

Premises used: dist_eq_norm, MeasureTheory.integral_sub, MeasureTheory.norm_integral_le_lintegral_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a - g a‖ ∂μ).toReal ≤ (∫⁻ (a : α), edist (f a) (g a) ∂μ).toReal

Tactic:
simp [edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
rw : ENNReal.ofReal (dist.{u_5} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)) ≤ ∫⁻ (a : α), edist (f a) (g a) ∂μ
⊢ edist.{u_5} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ≤ ∫⁻ (a : α), edist (f a) (g a) ∂μ

Tactic:
rw [edist_dist]

Premises used: edist_dist
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ENNReal.ofReal (dist.{u_5} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)) ≤ ∫⁻ (a : α), edist (f a) (g a) ∂μ

Tactic:
ENNReal.ofReal_le_of_le_toReal (dist_integral_le_lintegral_edist hf hg)

Premises used: MeasureTheory.dist_integral_le_lintegral_edist, ENNReal.ofReal_le_of_le_toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ENNReal.ofReal (dist.{u_5} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)) ≤ ∫⁻ (a : α), edist (f a) (g a) ∂μ

Tactic:
exact ENNReal.ofReal_le_of_le_toReal (dist_integral_le_lintegral_edist hf hg)

Premises used: MeasureTheory.dist_integral_le_lintegral_edist, ENNReal.ofReal_le_of_le_toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : f =ᶠ[ae μ] 0
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), f a ∂μ) 0

Tactic:
simp [integral_congr_ae hf, integral_zero]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.integral_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
h : Ne.{u_5 + 1} (α := G) (∫ (a : α), f a ∂μ) 0
⊢ ∃ᵐ (a : α) ∂μ, f a ≠ 0

Tactic:
fun h' ↦ h (integral_eq_zero_of_ae (h'.mono fun _ ↦ not_not.mp))

Premises used: Classical.not_not, Filter.Frequently, Filter.Eventually.mono, Iff.mp, MeasureTheory.integral_eq_zero_of_ae, Not
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
h : Ne.{u_5 + 1} (α := G) (∫ (a : α), f a ∂μ) 0
⊢ ∃ (a : α), f a ≠ 0

Tactic:
(frequently_ae_ne_zero_of_integral_ne_zero h).exists

Premises used: Filter.Frequently.exists, MeasureTheory.frequently_ae_ne_zero_of_integral_ne_zero
-- 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
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) l (𝓝 0)
rw : Tendsto (β := ℝ) (fun (x : ι) ↦ Norm.norm.{u_5} (E := G) (∫ (x : α) in s x, f x ∂μ)) l (𝓝 0)
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α) in s i, f x ∂μ) l (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- 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
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) l (𝓝 0)
simp_rw : Tendsto (β := ℝ≥0∞) (fun (a : ι) ↦ (↑(nnnorm.{u_5} (E := G) (∫ (x : α) in s a, f x ∂μ)) : ℝ≥0∞)) l (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ι) ↦ Norm.norm.{u_5} (E := G) (∫ (x : α) in s x, f x ∂μ)) l (𝓝 0)

Tactic:
simp_rw [← coe_nnnorm, ← NNReal.coe_zero, NNReal.tendsto_coe, ← ENNReal.tendsto_coe,
    ENNReal.coe_zero]

Premises used: NNReal.coe_zero, ENNReal.coe_zero, ENNReal.tendsto_coe, coe_nnnorm, NNReal.tendsto_coe
-- 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
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (a : ι) ↦ (↑(nnnorm.{u_5} (E := G) (∫ (x : α) in s a, f x ∂μ)) : ℝ≥0∞)) l (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (tendsto_setLIntegral_zero (ne_of_lt hf) hs) (fun i => zero_le)
    fun i => enorm_integral_le_lintegral_enorm _

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, MeasureTheory.enorm_integral_le_lintegral_enorm, ne_of_lt, MeasureTheory.tendsto_setLIntegral_zero
-- 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
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (a : ι) ↦ (↑(nnnorm.{u_5} (E := G) (∫ (x : α) in s a, f x ∂μ)) : ℝ≥0∞)) l (𝓝 0)

Tactic:
exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (tendsto_setLIntegral_zero (ne_of_lt hf) hs) (fun i => zero_le)
    fun i => enorm_integral_le_lintegral_enorm _

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, MeasureTheory.enorm_integral_le_lintegral_enorm, ne_of_lt, MeasureTheory.tendsto_setLIntegral_zero
-- 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
hf : Integrable f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (β := ℝ≥0∞) ((⇑μ : (a : Set α) → ℝ≥0∞) ∘ s) l (𝓝 0)
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α) in s i, f x ∂μ) l (𝓝 0)

Tactic:
hf.2.tendsto_setIntegral_nhds_zero hs

Premises used: MeasureTheory.HasFiniteIntegral.tendsto_setIntegral_nhds_zero, And.right
-- 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)
simp : Tendsto (fun (i : ι) ↦ setToFun μ (weightedSMul μ) ⋯ (F i)) l (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f 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 α
ι : 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)
⊢ Tendsto (fun (i : ι) ↦ setToFun μ (weightedSMul μ) ⋯ (F i)) l (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))

Tactic:
tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ) f hfi hFi hF

Premises used: MeasureTheory.tendsto_setToFun_of_L1, 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 α
ι : 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)
⊢ Tendsto (fun (i : ι) ↦ setToFun μ (weightedSMul μ) ⋯ (F i)) l (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))

Tactic:
exact tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ) f hfi hFi hF

Premises used: MeasureTheory.tendsto_setToFun_of_L1, 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 α
ι : 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)
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
tendsto_integral_of_L1 f hfi hFi ?_

Premises used: MeasureTheory.tendsto_integral_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)
refine : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
refine tendsto_integral_of_L1 f hfi hFi ?_

Premises used: MeasureTheory.tendsto_integral_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)
⊢ 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) μ
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) μ
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 α
ι : 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 α
⊢ Tendsto.{u_6, u_5} (β := G) (fun (i : ι) ↦ ∫ (x : α) in s, F i x ∂μ) l (𝓝 (∫ (x : α) in s, f x ∂μ))

Tactic:
tendsto_integral_of_L1 f hfi.restrict ?_ ?_

Premises used: MeasureTheory.tendsto_integral_of_L1, MeasureTheory.AEStronglyMeasurable.restrict
-- 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_1 : ∀ᶠ (i : ι) in l, Integrable (F i) (μ.restrict s)
refine_2 : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ ∫⁻ (x : α) in s, ‖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_integral_of_L1 f hfi.restrict ?_ ?_

Premises used: MeasureTheory.tendsto_integral_of_L1, MeasureTheory.AEStronglyMeasurable.restrict
-- 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 α
i : ι
hi : Integrable (F i) μ
⊢ Integrable (F i) (μ.restrict s)

Tactic:
hi.restrict

Premises used: MeasureTheory.Integrable.restrict
-- 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 α
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ Integrable (F i) μ) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ Integrable (F i) (μ.restrict s)) x} x}
      a
h₁ h₂ : ∀ (i : ι) (hi : Integrable (F i) μ), Integrable (F i) (μ.restrict s)
⊢ ∀ᶠ (i : ι) in l, Integrable (F i) (μ.restrict s)

Tactic:
filter_upwards [hFi] with i hi using hi.restrict