awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
hG : ¬CompleteSpace G
neg :
  sorry μ (fun (x : X) ↦ f x + g x) B =
    HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ g x) B)
⊢ ∫ᵛ (x : X), f x + g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
⊢ ∫ᵛ (x : X), (f + g) x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), g x ∂[B; μ]

Tactic:
integral_fun_add hf hg

Premises used: MeasureTheory.VectorMeasure.integral_fun_add
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Finset ι
f : ι → X → E
hf : ∀ i ∈ s, μ.Integrable (f i) B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]
⊢ ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Finset ι
f : ι → X → E
hf : ∀ i ∈ s, μ.Integrable (f i) B
hG : CompleteSpace G
pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ ∑ i ∈ s, f i x) B) (∑ x ∈ s, sorry μ (fun (x_1 : X) ↦ f x x_1) B)
⊢ ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]

Tactic:
simp only [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Finset ι
f : ι → X → E
hf : ∀ i ∈ s, μ.Integrable (f i) B
hG : CompleteSpace G
⊢ Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ ∑ i ∈ s, f i x) B) (∑ x ∈ s, sorry μ (fun (x_1 : X) ↦ f x x_1) B)

Tactic:
setToFun_finsetSum (dominatedFinMeasAdditive_cbmApplyMeasure μ B) s hf

Premises used: Unit.unit, sorryAx, MeasureTheory.setToFun_finsetSum, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Finset ι
f : ι → X → E
hf : ∀ i ∈ s, μ.Integrable (f i) B
hG : ¬CompleteSpace G
neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ ∑ i ∈ s, f i x) B) (∑ x ∈ s, sorry μ (fun (x_1 : X) ↦ f x x_1) B)
⊢ ∫ᵛ (x : X), ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ (x : X), f i x ∂[B; μ]

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
⊢ ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hG : CompleteSpace G
pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ -f x) B) (-sorry μ (fun (x : X) ↦ f x) B)
⊢ ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
simp only [integral, hG, ↓reduceDIte, transpose_eq_cbmApplyMeasure]

Premises used: MeasureTheory.transpose_eq_cbmApplyMeasure, reduceDIte, MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hG : CompleteSpace G
⊢ Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ -f x) B) (-sorry μ (fun (x : X) ↦ f x) B)

Tactic:
setToFun_neg (dominatedFinMeasAdditive_cbmApplyMeasure μ B) f

Premises used: Unit.unit, sorryAx, MeasureTheory.setToFun_neg, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hG : ¬CompleteSpace G
neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ -f x) B) (-sorry μ (fun (x : X) ↦ f x) B)
⊢ ∫ᵛ (x : X), -f x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ ∫ᵛ (x : X), (-f) x ∂[B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
integral_fun_neg f μ B

Premises used: MeasureTheory.VectorMeasure.integral_fun_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]
⊢ ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
hG : CompleteSpace G
pos :
  sorry μ (fun (x : X) ↦ f x - g x) B =
    HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ g x) B)
⊢ ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]

Tactic:
simp only [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
hG : CompleteSpace G
⊢ sorry μ (fun (x : X) ↦ f x - g x) B =
    HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ g x) B)

Tactic:
setToFun_sub (dominatedFinMeasAdditive_cbmApplyMeasure μ B) hf hg

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, MeasureTheory.setToFun_sub, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
hG : ¬CompleteSpace G
neg :
  sorry μ (fun (x : X) ↦ f x - g x) B =
    HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ g x) B)
⊢ ∫ᵛ (x : X), f x - g x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f B
hg : μ.Integrable g B
⊢ ∫ᵛ (x : X), (f - g) x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), g x ∂[B; μ]

Tactic:
integral_fun_sub hf hg

Premises used: MeasureTheory.VectorMeasure.integral_fun_sub
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
c : ℝ
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
⊢ ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
c : ℝ
hG : CompleteSpace G
pos : sorry μ (fun (x : X) ↦ c • f x) B = HSMul.hSMul (β := G) c (sorry μ (fun (x : X) ↦ f x) B)
⊢ ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
simp only [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
c : ℝ
hG : CompleteSpace G
simp :
  ∀ (c : ℝ) (s : Set X) (x : E),
    HSMul.hSMul (β := ?m.104) c ((?m.112 s : (a : E) → ?m.104) x : ?m.104) =
      HSMul.hSMul (β := ?m.104) c ((?m.112 s : (a : E) → ?m.104) x : ?m.104)
⊢ ∀ (c : ℝ) (s : Set X) (x : E),
    (?m.112 s : (a : E) → ?m.104) (c • x) = HSMul.hSMul (β := ?m.104) c ((?m.112 s : (a : E) → ?m.104) x : ?m.104)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
c : ℝ
hG : ¬CompleteSpace G
neg : sorry μ (fun (x : X) ↦ c • f x) B = HSMul.hSMul (β := G) c (sorry μ (fun (x : X) ↦ f x) B)
⊢ ∫ᵛ (x : X), c • f x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
c : ℝ
⊢ ∫ᵛ (x : X), (c • f) x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
integral_fun_smul f μ B c

Premises used: MeasureTheory.VectorMeasure.integral_fun_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
simp : Eq.{u_5 + 1} (α := G) (sorry 0 (fun (x : X) ↦ f x) B) 0
⊢ ∫ᵛ (x : X), f x ∂[B; 0] = 0

Tactic:
simp [integral]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst_6 : IsEmpty X
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = 0

Tactic:
simp [eq_zero_of_isEmpty]

Premises used: MeasureTheory.VectorMeasure.eq_zero_of_isEmpty
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hμ : μ.Integrable f B
hν : ν.Integrable f B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]
⊢ ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hμ : μ.Integrable f B
hν : ν.Integrable f B
hG : CompleteSpace G
pos :
  sorry (μ + ν) (fun (x : X) ↦ f x) B =
    HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry ν (fun (x : X) ↦ f x) B)
⊢ ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]

Tactic:
simp only [integral, hG, ↓reduceDIte, transpose_add_vectorMeasure, coe_add,
      transpose_eq_cbmApplyMeasure, ← setToFun_add_measure
        (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
        (dominatedFinMeasAdditive_cbmApplyMeasure ν B) hμ hν]

Premises used: MeasureTheory.transpose_eq_cbmApplyMeasure, reduceDIte, MeasureTheory.VectorMeasure.coe_add, MeasureTheory.VectorMeasure.transpose_add_vectorMeasure, MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hμ : μ.Integrable f B
hν : ν.Integrable f B
hG : CompleteSpace G
⊢ sorry (μ + ν) (fun (x : X) ↦ f x) B =
    HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry ν (fun (x : X) ↦ f x) B)

Tactic:
(setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm

Premises used: OfNat.ofNat, Eq.symm, MeasureTheory.setToFun_congr_measure_of_integrable, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hμ : μ.Integrable f B
hν : ν.Integrable f B
hG : ¬CompleteSpace G
neg :
  sorry (μ + ν) (fun (x : X) ↦ f x) B =
    HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry ν (fun (x : X) ↦ f x) B)
⊢ ∫ᵛ (x : X), f x ∂[B; μ + ν] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
hG : CompleteSpace G
pos : ∀ (hs : s.Nonempty), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
neg : ∀ (hs : s = ∅), ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]

Tactic:
by_cases! hs : s.Nonempty

Premises used: Finset.Nonempty
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
hG : CompleteSpace G
hs : s.Nonempty
pos : Eq.{u_5 + 1} (α := G) (sorry (∑ i ∈ s, μ i) (fun (x : X) ↦ f x) B) (∑ x ∈ s, sorry (μ x) (fun (x : X) ↦ f x) B)
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]

Tactic:
simp only [integral, hG, ↓reduceDIte, transpose_finsetSum_vectorMeasure, coe_finsetSum,
        transpose_eq_cbmApplyMeasure, ← setToFun_finsetSum_measure hs
          (fun i ↦ dominatedFinMeasAdditive_cbmApplyMeasure (μ i) B) hf]

Premises used: MeasureTheory.VectorMeasure.coe_finsetSum, MeasureTheory.transpose_eq_cbmApplyMeasure, reduceDIte, MeasureTheory.VectorMeasure.integral, MeasureTheory.VectorMeasure.transpose_finsetSum_vectorMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
hG : CompleteSpace G
hs : s.Nonempty
⊢ Eq.{u_5 + 1} (α := G) (sorry (∑ i ∈ s, μ i) (fun (x : X) ↦ f x) B) (∑ x ∈ s, sorry (μ x) (fun (x : X) ↦ f x) B)

Tactic:
(setToFun_congr_measure_of_integrable 1 ENNReal.one_ne_top ?_ _ _ f ?_).symm

Premises used: OfNat.ofNat, Eq.symm, MeasureTheory.setToFun_congr_measure_of_integrable, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
hG : CompleteSpace G
hs : s = ∅
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
s : Finset ι
hf : ∀ i ∈ s, (μ i).Integrable f B
hG : ¬CompleteSpace G
neg : Eq.{u_5 + 1} (α := G) (sorry (∑ i ∈ s, μ i) (fun (x : X) ↦ f x) B) (∑ x ∈ s, sorry (μ x) (fun (x : X) ↦ f x) B)
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B; μ i]

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Integral
Goal:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; -μ] = -∫ᵛ (x : X), f x ∂[B; μ]
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; -μ] = -∫ᵛ (x : X), f x ∂[B; μ]
⊢ ∫ᵛ (x : X), f x ∂[B; -μ] = -∫ᵛ (x : X), f x ∂[B; μ]

Tactic:
by_cases hG : CompleteSpace G

Premises used: CompleteSpace