awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : TopologicalSpace α
f : α → ℝ
hs : IsConnected s
hf : ContinuousOn f s
hint : IntegrableOn f s μ
hμfin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ave : ℝ := ⨍ (x : α) in s, f x ∂μ
S₁ : Set α := {x : α | x ∈ s ∧ f x ≤ ave}
S₂ : Set α := {x : α | x ∈ s ∧ ave ≤ f x}
hS₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₁ : ℝ≥0∞)
hS₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₂ : ℝ≥0∞)
c₁ : α
hc₁ : c₁ ∈ S₁
rcases : ∀ (c₂ : α) (hc₂ : c₂ ∈ S₂), ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ

Tactic:
rcases nonempty_of_measure_ne_zero hS₂.ne' with ⟨c₂, hc₂⟩

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : TopologicalSpace α
f : α → ℝ
hs : IsConnected s
hf : ContinuousOn f s
hint : IntegrableOn f s μ
hμfin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ave : ℝ := ⨍ (x : α) in s, f x ∂μ
S₁ : Set α := {x : α | x ∈ s ∧ f x ≤ ave}
S₂ : Set α := {x : α | x ∈ s ∧ ave ≤ f x}
hS₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₁ : ℝ≥0∞)
hS₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₂ : ℝ≥0∞)
c₁ : α
hc₁ : c₁ ∈ S₁
c₂ : α
hc₂ : c₂ ∈ S₂
a : ⨍ (x : α) in s, f x ∂μ ∈ Icc (f c₁) (f c₂)
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ

Tactic:
apply hs.isPreconnected.intermediate_value hc₁.1 hc₂.1 hf

Premises used: And.left, IsConnected.isPreconnected, IsPreconnected.intermediate_value
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : TopologicalSpace α
f : α → ℝ
hs : IsConnected s
hf : ContinuousOn f s
hint : IntegrableOn f s μ
hμfin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ave : ℝ := ⨍ (x : α) in s, f x ∂μ
S₁ : Set α := {x : α | x ∈ s ∧ f x ≤ ave}
S₂ : Set α := {x : α | x ∈ s ∧ ave ≤ f x}
hS₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₁ : ℝ≥0∞)
hS₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₂ : ℝ≥0∞)
c₁ : α
hc₁ : c₁ ∈ S₁
c₂ : α
hc₂ : c₂ ∈ S₂
⊢ ⨍ (x : α) in s, f x ∂μ ∈ Icc (f c₁) (f c₂)

Tactic:
grind
-- 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
f : α → E
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = L1.integral (Integrable.toL1 f hf)

Tactic:
simp [integral, hE, hf]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
pos : ∀ (hE : CompleteSpace E), ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f
neg : ∀ (hE : ¬CompleteSpace E), ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f
⊢ ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hE : CompleteSpace E
pos :
  Eq.{u_2 + 1} (α := E)
    (if hf : Integrable.{u_2, u_1} (ε := E) (fun (a : α) ↦ f a) μ then
      (L1.integralCLM : (a : ↥(Lp E 1 μ)) → E) (Integrable.toL1 (fun (a : α) ↦ f a) hf)
    else 0)
    (if hf : Integrable f μ then (L1.setToL1 ⋯ : (a : ↥(Lp E 1 μ)) → E) (Integrable.toL1 f hf) else 0)
⊢ ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f

Tactic:
simp only [integral, hE, ↓reduceDIte, L1.integral, setToFun]

Premises used: reduceDIte, MeasureTheory.integral, MeasureTheory.L1.integral, MeasureTheory.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 α
f : α → E
hE : CompleteSpace E
⊢ Eq.{u_2 + 1} (α := E)
    (if hf : Integrable.{u_2, u_1} (ε := E) (fun (a : α) ↦ f a) μ then
      (L1.integralCLM : (a : ↥(Lp E 1 μ)) → E) (Integrable.toL1 (fun (a : α) ↦ f a) hf)
    else 0)
    (if hf : Integrable f μ then (L1.setToL1 ⋯ : (a : ↥(Lp E 1 μ)) → E) (Integrable.toL1 f hf) else 0)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hE : ¬CompleteSpace E
⊢ ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f

Tactic:
simp [integral, hE, setToFun]

Premises used: MeasureTheory.integral, MeasureTheory.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 α
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
simp : (integralCLM : (a : ↥(Lp E 1 μ)) → E) f = setToFun μ (weightedSMul μ) ⋯ (↑(↑f : α →ₘ[μ] E) : α → E)
⊢ integral f = ∫ (a : α), (↑(↑f : α →ₘ[μ] E) : α → E) a ∂μ

Tactic:
simp only [integral, L1.integral, integral_eq_setToFun]

Premises used: MeasureTheory.integral_eq_setToFun, MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ (integralCLM : (a : ↥(Lp E 1 μ)) → E) f = setToFun μ (weightedSMul μ) ⋯ (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
(L1.setToFun_eq_setToL1 (dominatedFinMeasAdditive_weightedSMul μ) f).symm

Premises used: Set.Mem, MeasureTheory.L1.setToFun_eq_setToL1, MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.SimpleFunc.integral, MeasureTheory.L1.SimpleFunc.integralCLM', Eq.symm, 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 α
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ (integralCLM : (a : ↥(Lp E 1 μ)) → E) f = setToFun μ (weightedSMul μ) ⋯ (↑(↑f : α →ₘ[μ] E) : α → E)

Tactic:
exact (L1.setToFun_eq_setToL1 (dominatedFinMeasAdditive_weightedSMul μ) f).symm

Premises used: MeasureTheory.L1.setToFun_eq_setToL1, Eq.symm, 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
h : ¬Integrable f μ
simp : setToFun μ (weightedSMul μ) ⋯ f = 0
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), f a ∂μ) 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 α
μ : Measure α
f : α → G
h : ¬Integrable f μ
⊢ setToFun μ (weightedSMul μ) ⋯ f = 0

Tactic:
setToFun_undef (dominatedFinMeasAdditive_weightedSMul μ) h

Premises used: MeasureTheory.setToFun_undef, 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
h : ¬Integrable f μ
⊢ setToFun μ (weightedSMul μ) ⋯ f = 0

Tactic:
exact setToFun_undef (dominatedFinMeasAdditive_weightedSMul μ) h

Premises used: MeasureTheory.setToFun_undef, 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
h : Ne.{u_5 + 1} (α := G) (∫ (a : α), f a ∂μ) 0
⊢ Integrable f μ

Tactic:
Not.imp_symm integral_undef h

Premises used: MeasureTheory.integral_undef, Not.imp_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
h : ¬AEStronglyMeasurable f μ
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), f a ∂μ) 0

Tactic:
integral_undef <| not_and_of_not_left _ h

Premises used: MeasureTheory.integral_undef, not_and_of_not_left
-- 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 : Eq.{u_5 + 1} (α := G) (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ 0) 0
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : α), 0 ∂μ) 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 α
μ : Measure α
⊢ Eq.{u_5 + 1} (α := G) (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ 0) 0

Tactic:
apply setToFun_zero

Premises used: MeasureTheory.setToFun_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 α
⊢ Eq.{u_5 + 1} (α := G) (integral μ 0) 0

Tactic:
integral_zero α G

Premises used: 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 α
β : Type u_6
f : β → α → G
s : Set β
b : β
pos :
  ∀ (hb : b ∈ s),
    Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
      (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)
neg :
  ∀ (hb : b ∉ s),
    Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
      (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)
⊢ Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
    (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)

Tactic:
by_cases hb : b ∈ s
-- 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
s : Set β
b : β
hb : b ∈ s
⊢ Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
    (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)

Tactic:
simp [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
f : β → α → G
s : Set β
b : β
hb : b ∉ s
⊢ Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
    (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)

Tactic:
simp [hb]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : Eq (α := ℝ) (∫ (x : α), f x ∂μ) 1
⊢ Integrable f μ

Tactic:
.of_integral_ne_zero <| h ▸ one_ne_zero

Premises used: MeasureTheory.Integrable.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 α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
simp :
  (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ f a + g a) =
    setToFun μ (weightedSMul μ) ⋯ f + setToFun μ (weightedSMul μ) ⋯ g
⊢ ∫ (a : α), f a + g a ∂μ = HAdd.hAdd (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), 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 α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ f a + g a) =
    setToFun μ (weightedSMul μ) ⋯ f + setToFun μ (weightedSMul μ) ⋯ g

Tactic:
setToFun_add (dominatedFinMeasAdditive_weightedSMul μ) hf hg

Premises used: MeasureTheory.setToFun_add, 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 : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ f a + g a) =
    setToFun μ (weightedSMul μ) ⋯ f + setToFun μ (weightedSMul μ) ⋯ g

Tactic:
exact setToFun_add (dominatedFinMeasAdditive_weightedSMul μ) hf hg

Premises used: MeasureTheory.setToFun_add, 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 : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫ (a : α), (f + g) a ∂μ = HAdd.hAdd (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)

Tactic:
integral_add hf hg

Premises used: MeasureTheory.integral_add
-- 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
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
simp :
  Eq.{u_5 + 1} (α := G) (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ ∑ i ∈ s, f i a)
    (∑ x ∈ s, setToFun μ (weightedSMul μ) ⋯ (f x))
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), ∑ i ∈ s, f i a ∂μ) (∑ i ∈ s, ∫ (a : α), f i 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 α
ι : Type u_6
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ Eq.{u_5 + 1} (α := G) (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ ∑ i ∈ s, f i a)
    (∑ x ∈ s, setToFun μ (weightedSMul μ) ⋯ (f x))

Tactic:
setToFun_finsetSum (dominatedFinMeasAdditive_weightedSMul _) s hf

Premises used: MeasureTheory.setToFun_finsetSum, 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
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ Eq.{u_5 + 1} (α := G) (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ ∑ i ∈ s, f i a)
    (∑ x ∈ s, setToFun μ (weightedSMul μ) ⋯ (f x))

Tactic:
exact setToFun_finsetSum (dominatedFinMeasAdditive_weightedSMul _) s hf

Premises used: MeasureTheory.setToFun_finsetSum, 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 μ) ⋯ fun (a : α) ↦ -f a) = -setToFun μ (weightedSMul μ) ⋯ f
⊢ Eq.{u_5 + 1} (α := 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
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ -f a) = -setToFun μ (weightedSMul μ) ⋯ f

Tactic:
setToFun_neg (dominatedFinMeasAdditive_weightedSMul μ) f

Premises used: MeasureTheory.setToFun_neg, 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
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ -f a) = -setToFun μ (weightedSMul μ) ⋯ f

Tactic:
exact setToFun_neg (dominatedFinMeasAdditive_weightedSMul μ) f

Premises used: MeasureTheory.setToFun_neg, 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
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), (-f) a ∂μ) (-∫ (a : α), f a ∂μ)

Tactic:
integral_neg f

Premises used: MeasureTheory.integral_neg
-- 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 μ
simp :
  (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ f a - g a) =
    setToFun μ (weightedSMul μ) ⋯ f - setToFun μ (weightedSMul μ) ⋯ g
⊢ ∫ (a : α), f a - g a ∂μ = HSub.hSub (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), 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 α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ f a - g a) =
    setToFun μ (weightedSMul μ) ⋯ f - setToFun μ (weightedSMul μ) ⋯ g

Tactic:
setToFun_sub (dominatedFinMeasAdditive_weightedSMul μ) hf hg

Premises used: MeasureTheory.setToFun_sub, 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 : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ f a - g a) =
    setToFun μ (weightedSMul μ) ⋯ f - setToFun μ (weightedSMul μ) ⋯ g

Tactic:
exact setToFun_sub (dominatedFinMeasAdditive_weightedSMul μ) hf hg

Premises used: MeasureTheory.setToFun_sub, 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 : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫ (a : α), (f - g) a ∂μ = HSub.hSub (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)

Tactic:
integral_sub hf hg

Premises used: MeasureTheory.integral_sub
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
𝕜 : Type u_4
inst : NormedDivisionRing 𝕜
G : Type u_5
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst_3 : Module 𝕜 G
inst_4 : NormSMulClass 𝕜 G
inst_5 : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
simp : (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ c • f a) = c • setToFun μ (weightedSMul μ) ⋯ f
⊢ ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (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
𝕜 : Type u_4
inst : NormedDivisionRing 𝕜
G : Type u_5
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst_3 : Module 𝕜 G
inst_4 : NormSMulClass 𝕜 G
inst_5 : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ c • f a) = c • setToFun μ (weightedSMul μ) ⋯ f

Tactic:
setToFun_smul (dominatedFinMeasAdditive_weightedSMul μ) weightedSMul_smul c f

Premises used: MeasureTheory.setToFun_smul, MeasureTheory.weightedSMul_smul, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
𝕜 : Type u_4
inst : NormedDivisionRing 𝕜
G : Type u_5
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst_3 : Module 𝕜 G
inst_4 : NormSMulClass 𝕜 G
inst_5 : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
⊢ (setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ c • f a) = c • setToFun μ (weightedSMul μ) ⋯ f

Tactic:
exact setToFun_smul (dominatedFinMeasAdditive_weightedSMul μ) weightedSMul_smul c f

Premises used: MeasureTheory.setToFun_smul, MeasureTheory.weightedSMul_smul, 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 α
R : Type u_6
inst_2 : NormedRing R
inst_3 : Module R G
inst_4 : IsBoundedSMul R G
inst_5 : SMulCommClass ℝ R G
c : R
f : α → G
hf : Integrable f μ
pos : ∀ (hG : CompleteSpace G), ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)
neg : ∀ (hG : ¬CompleteSpace G), ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)
⊢ ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
R : Type u_6
inst_2 : NormedRing R
inst_3 : Module R G
inst_4 : IsBoundedSMul R G
inst_5 : SMulCommClass ℝ R G
c : R
f : α → G
hf : Integrable f μ
hG : CompleteSpace G
⊢ ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)

Tactic:
simpa only [integral, hG, hf, hf.fun_smul c] using L1.integral_smul c (toL1 f hf)

Premises used: MeasureTheory.L1.integral_smul, MeasureTheory.integral, MeasureTheory.Integrable.fun_smul, MeasureTheory.Integrable.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 α
R : Type u_6
inst_2 : NormedRing R
inst_3 : Module R G
inst_4 : IsBoundedSMul R G
inst_5 : SMulCommClass ℝ R G
c : R
f : α → G
hf : Integrable f μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
L : Type u_6
inst : RCLike L
r : L
f : α → L
⊢ ∫ (a : α), r * f a ∂μ = r * ∫ (a : α), f a ∂μ

Tactic:
integral_smul r f

Premises used: MeasureTheory.integral_smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
L : Type u_6
inst : RCLike L
r : L
f : α → L
⊢ ∫ (a : α), f a * r ∂μ = (∫ (a : α), f a ∂μ) * r

Tactic:
simp only [mul_comm, integral_const_mul r f]

Premises used: MeasureTheory.integral_const_mul, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
L : Type u_6
inst : RCLike L
r : L
f : α → L
⊢ ∫ (a : α), f a / r ∂μ = (∫ (a : α), f a ∂μ) / r

Tactic:
simpa only [← div_eq_mul_inv] using integral_mul_const r⁻¹ f

Premises used: div_eq_mul_inv, Inv.inv, MeasureTheory.integral_mul_const
-- 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
simp : setToFun μ (weightedSMul μ) ⋯ f = setToFun μ (weightedSMul μ) ⋯ g
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), 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 α
f g : α → G
h : f =ᶠ[ae μ] g
⊢ setToFun μ (weightedSMul μ) ⋯ f = setToFun μ (weightedSMul μ) ⋯ g

Tactic:
setToFun_congr_ae (dominatedFinMeasAdditive_weightedSMul μ) h

Premises used: MeasureTheory.setToFun_congr_ae, MeasureTheory.dominatedFinMeasAdditive_weightedSMul