awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
hf : Integrable f μ
⊢ Eq (α := ℝ) (∫ (a : α), ‖(↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] H) : α → H) a‖ ∂μ) (∫ (a : α), ‖f a‖ ∂μ)

Tactic:
integral_congr_ae <| hf.coeFn_toL1.fun_comp _

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.Integrable.coeFn_toL1, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
hf : Integrable f μ
⊢ Eq (α := ℝ) (∫ (a : α), ‖(↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] H) : α → H) a‖ ∂μ) (∫ (a : α), ‖f a‖ ∂μ)

Tactic:
exact integral_congr_ae <| hf.coeFn_toL1.fun_comp _

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.Integrable.coeFn_toL1, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
simp_rw : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ p.toReal ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ

Tactic:
simp_rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm]

Premises used: ENNReal.ofReal_rpow_of_nonneg, ENNReal.toReal_nonneg, ofReal_norm, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ

Tactic:
have A : ∫⁻ a : α, ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ a : α, ‖f a‖ₑ ^ p.toReal ∂μ := by
    simp_rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
simp :
  (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal (HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) p.toReal⁻¹)
⊢ eLpNorm f p μ = ENNReal.ofReal (HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) p.toReal⁻¹)

Tactic:
simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal hp1 hp2, one_div]

Premises used: one_div, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
rw :
  (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p.toReal
hfm : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p.toReal) μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal (HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) p.toReal⁻¹)

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae]

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
x : α
⊢ LE.le (α := ℝ) (0 x) ((fun (a : α) ↦ ‖f a‖ ^ p.toReal) x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p.toReal

Tactic:
exact ae_of_all _ fun x => by positivity

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p.toReal) μ

Tactic:
(hf.aestronglyMeasurable.norm.aemeasurable.pow_const _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p.toReal) μ

Tactic:
exact (hf.aestronglyMeasurable.norm.aemeasurable.pow_const _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)

Tactic:
rw [A, ← ofReal_rpow_of_nonneg toReal_nonneg (inv_nonneg.2 toReal_nonneg), ofReal_toReal]

Premises used: Iff.mpr, ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_toReal, ENNReal.toReal_nonneg, inv_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞

Tactic:
(lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp1 hp2 hf.2).ne

Premises used: And.right, MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞

Tactic:
exact (lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp1 hp2 hf.2).ne

Premises used: And.right, MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top, LT.lt.ne
-- 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
⊢ ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖

Tactic:
have le_ae : ∀ᵐ a ∂μ, 0 ≤ ‖f a‖ := Eventually.of_forall fun a => norm_nonneg _
-- 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_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
pos : ∀ (h : AEStronglyMeasurable f μ), norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ
neg : ∀ (h : ¬AEStronglyMeasurable f μ), norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
by_cases h : AEStronglyMeasurable f μ

Premises used: MeasureTheory.AEStronglyMeasurable
-- 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_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : AEStronglyMeasurable f μ
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
norm_integral_le_lintegral_norm _

Premises used: 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
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = ∫ (a : α), ‖f a‖ ∂μ

Tactic:
(integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm).symm

Premises used: MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Eq.symm
-- 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_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : AEStronglyMeasurable f μ
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
calc
      ‖∫ a, f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) :=
        norm_integral_le_lintegral_norm _
      _ = ∫ a, ‖f a‖ ∂μ := (integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm).symm

Premises used: Norm.norm, ENNReal.ofReal, MeasureTheory.norm_integral_le_lintegral_norm, MeasureTheory.AEStronglyMeasurable.norm, ENNReal.toReal, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Eq.symm, MeasureTheory.lintegral
-- 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_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ
neg : LE.le (α := ℝ) 0 (∫ (a : α), ‖f a‖ ∂μ)
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
rw [integral_non_aestronglyMeasurable h, norm_zero]

Premises used: MeasureTheory.integral_non_aestronglyMeasurable, norm_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
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ
⊢ LE.le (α := ℝ) 0 (∫ (a : α), ‖f a‖ ∂μ)

Tactic:
integral_nonneg_of_ae le_ae

Premises used: MeasureTheory.integral_nonneg_of_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 α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ
⊢ LE.le (α := ℝ) 0 (∫ (a : α), ‖f a‖ ∂μ)

Tactic:
exact integral_nonneg_of_ae le_ae

Premises used: MeasureTheory.integral_nonneg_of_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ LE.le (α := ℝ) |∫ (a : α), f a ∂μ| (∫ (a : α), |f a| ∂μ)

Tactic:
norm_integral_le_integral_norm f

Premises used: MeasureTheory.norm_integral_le_integral_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 : α → ℝ
hg : Integrable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x
⊢ norm.{u_5} (E := G) (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g x ∂μ

Tactic:
calc
    ‖∫ x, f x ∂μ‖ ≤ ∫ x, ‖f x‖ ∂μ := norm_integral_le_integral_norm f
    _ ≤ ∫ x, g x ∂μ := integral_mono_of_nonneg (Eventually.of_forall fun _ => norm_nonneg _) hg h

Premises used: Trans.trans, MeasureTheory.norm_integral_le_integral_norm, Filter.Eventually.of_forall, MeasureTheory.integral_mono_of_nonneg, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
pos : ∀ (hμ : IsFiniteMeasure μ), ∫ (x : α), c ∂μ = μ.real univ • c
neg : ∀ (hμ : ¬IsFiniteMeasure μ), ∫ (x : α), c ∂μ = μ.real univ • c
⊢ ∫ (x : α), c ∂μ = μ.real univ • c

Tactic:
by_cases hμ : IsFiniteMeasure μ

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : IsFiniteMeasure μ
pos : (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ c) = μ.real univ • c
⊢ ∫ (x : α), c ∂μ = μ.real univ • c

Tactic:
simp only [integral_eq_setToFun]

Premises used: MeasureTheory.integral_eq_setToFun
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : IsFiniteMeasure μ
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ c) = μ.real univ • c

Tactic:
setToFun_const (dominatedFinMeasAdditive_weightedSMul _) _

Premises used: MeasureTheory.setToFun_const, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : IsFiniteMeasure μ
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ c) = μ.real univ • c

Tactic:
exact setToFun_const (dominatedFinMeasAdditive_weightedSMul _) _

Premises used: MeasureTheory.setToFun_const, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : ¬IsFiniteMeasure μ
pos : ∀ (hc : c = 0), ∫ (x : α), c ∂μ = μ.real univ • c
neg : ∀ (hc : ¬c = 0), ∫ (x : α), c ∂μ = μ.real univ • c
⊢ ∫ (x : α), c ∂μ = μ.real univ • c

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : ¬IsFiniteMeasure μ
hc : c = 0
⊢ ∫ (x : α), c ∂μ = μ.real univ • c

Tactic:
simp [hc, integral_zero]

Premises used: MeasureTheory.integral_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : ¬IsFiniteMeasure μ
hc : ¬c = 0
⊢ ∫ (x : α), c ∂μ = μ.real univ • c

Tactic:
simp [measureReal_def, (integrable_const_iff_isFiniteMeasure hc).not.2 hμ,
      integral_undef, MeasureTheory.not_isFiniteMeasure_iff.mp hμ]

Premises used: Iff.mpr, MeasureTheory.integral_undef, Iff.not, MeasureTheory.not_isFiniteMeasure_iff, Iff.mp, MeasureTheory.measureReal_def, MeasureTheory.integrable_const_iff_isFiniteMeasure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst_2 : IsProbabilityMeasure μ
f : α → E
c : E
hf : ∀ᵐ (x : α) ∂μ, f x = c
⊢ ∫ (x : α), f x ∂μ = c

Tactic:
simp [integral_congr_ae hf]

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 α
inst_2 : IsFiniteMeasure μ
f : α → G
C : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
rw : μ.real univ • C = C * μ.real univ
rw₁ : μ.real univ * C = C * μ.real univ
rw₂ rw₃ : C * μ.real univ = C * μ.real univ
⊢ ∫ (x : α), C ∂μ = C * μ.real univ

Tactic:
rw [integral_const, smul_eq_mul, mul_comm]

Premises used: MeasureTheory.integral_const, mul_comm, smul_eq_mul
-- 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μ : Integrable f μ
hν : Integrable f ν
simp : setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f
⊢ ∫ (x : α), f x ∂(μ + ν) = HAdd.hAdd (α := G) (∫ (x : α), f x ∂μ) (∫ (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 α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
apply :
  ∀ (s : Set α) (hs : MeasurableSet s) (h's : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    weightedSMul (μ + ν) s = HAdd.hAdd (α := G →L[ℝ] G) (weightedSMul μ s) (weightedSMul ν s)
⊢ setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f

Tactic:
apply setToFun_add_left'' (fun s hs h's ↦ ?_) hμ hν le_rfl zero_le_one zero_le_one zero_le_one

Premises used: le_rfl, MeasureTheory.setToFun_add_left'', zero_le_one
-- 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μ : Integrable f μ
hν : Integrable f ν
s : Set α
hs : MeasurableSet s
h's : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [Measure.coe_add, Pi.add_apply, add_lt_top] at h's

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply, ENNReal.add_lt_top
-- 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μ : Integrable f μ
hν : Integrable f ν
s : Set α
hs : MeasurableSet s
h's :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ weightedSMul (μ + ν) s = HAdd.hAdd (α := G →L[ℝ] G) (weightedSMul μ s) (weightedSMul ν s)

Tactic:
simp [weightedSMul, Measure.real, toReal_add, h's.1.ne, h's.2.ne, add_smul]

Premises used: ENNReal.toReal_add, MeasureTheory.Measure.real, MeasureTheory.weightedSMul, And.right, add_smul, And.left, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
simp : setToFun (m := m) 0 (@weightedSMul _ _ _ _ m 0) ⋯ f = 0
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m 0 fun (x : α) ↦ f x) 0

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 α
f : α → G
⊢ setToFun (m := m) 0 (@weightedSMul _ _ _ _ m 0) ⋯ f = 0

Tactic:
setToFun_measure_zero (dominatedFinMeasAdditive_weightedSMul _) rfl

Premises used: MeasureTheory.setToFun_measure_zero, MeasureTheory.dominatedFinMeasAdditive_weightedSMul, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
⊢ setToFun (m := m) 0 (@weightedSMul _ _ _ _ m 0) ⋯ f = 0

Tactic:
exact setToFun_measure_zero (dominatedFinMeasAdditive_weightedSMul _) rfl

Premises used: MeasureTheory.setToFun_measure_zero, MeasureTheory.dominatedFinMeasAdditive_weightedSMul, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
μ : Measure α
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : α) in s, f x ∂μ) 0

Tactic:
Measure.restrict_eq_zero.mpr hs ▸ integral_zero_measure f

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero, Eq.rec, MeasureTheory.integral_zero_measure, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst_2 : IsEmpty α
f : α → G
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : α), f x ∂μ) 0

Tactic:
μ.eq_zero_of_isEmpty ▸ integral_zero_measure _

Premises used: Eq.rec, MeasureTheory.Measure.eq_zero_of_isEmpty, MeasureTheory.integral_zero_measure, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ ∅, μ i) fun (a : α) ↦ f a) (∑ i ∈ ∅, ∫ (a : α), f a ∂μ i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a : ι
s : Finset ι
h : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, Integrable f (μ i)),
    Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (a : α), f a ∂μ i)
hf : ∀ i ∈ Finset.cons a s h, Integrable f (μ i)
⊢ Integrable f (μ a) ∧ ∀ x ∈ s, Integrable f (μ x)

Tactic:
rw [Finset.forall_mem_cons] at hf

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a : ι
s : Finset ι
h : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, Integrable f (μ i)),
    Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (a : α), f a ∂μ i)
hf : Integrable f (μ a) ∧ ∀ x ∈ s, Integrable f (μ x)
cons :
  ∫ (a : α), f a ∂(μ a + ∑ x ∈ s, μ x) =
    HAdd.hAdd (α := G) (∫ (a : α), f a ∂μ a) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ Finset.cons a s h, μ i) fun (a : α) ↦ f a)
    (∑ i ∈ Finset.cons a s h, ∫ (a : α), f a ∂μ i)

Tactic:
rw [Finset.sum_cons, Finset.sum_cons, ← ih hf.2]

Premises used: Finset.sum_cons, And.right
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a : ι
s : Finset ι
h : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, Integrable f (μ i)),
    Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (a : α), f a ∂μ i)
hf : Integrable f (μ a) ∧ ∀ x ∈ s, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂(μ a + ∑ x ∈ s, μ x) =
    HAdd.hAdd (α := G) (∫ (a : α), f a ∂μ a) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a)

Tactic:
integral_add_measure hf.1 (integrable_finsetSum_measure.2 hf.2)

Premises used: Iff.mpr, MeasureTheory.integral_add_measure, MeasureTheory.integrable_finsetSum_measure, And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a : ι
s : Finset ι
h : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, Integrable f (μ i)),
    Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (a : α), f a ∂μ i)
hf : Integrable f (μ a) ∧ ∀ x ∈ s, Integrable f (μ x)
⊢ ∫ (a : α), f a ∂(μ a + ∑ x ∈ s, μ x) =
    HAdd.hAdd (α := G) (∫ (a : α), f a ∂μ a) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a)

Tactic:
exact integral_add_measure hf.1 (integrable_finsetSum_measure.2 hf.2)

Premises used: Iff.mpr, MeasureTheory.integral_add_measure, MeasureTheory.integrable_finsetSum_measure, And.right, And.left