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 : 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 [integral, hG, ← setToFun_neg']

Premises used: MeasureTheory.setToFun_neg', 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
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
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 =
    HSub.hSub (α := 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_sub_vectorMeasure, coe_sub,
      transpose_eq_cbmApplyMeasure, ← setToFun_sub_measure
        (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
        (dominatedFinMeasAdditive_cbmApplyMeasure ν B) hμ hν]

Premises used: MeasureTheory.VectorMeasure.transpose_sub_vectorMeasure, MeasureTheory.transpose_eq_cbmApplyMeasure, MeasureTheory.VectorMeasure.coe_sub, 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
hμ : μ.Integrable f B
hν : ν.Integrable f B
hG : CompleteSpace G
⊢ sorry (μ - ν) (fun (x : X) ↦ f x) B =
    HSub.hSub (α := 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 =
    HSub.hSub (α := 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:
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
simp : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) 0) 0
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]
⊢ ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]

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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : CompleteSpace G
pos :
  sorry μ (fun (x : X) ↦ f x) (B + C) =
    HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)
⊢ ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]

Tactic:
simp only [integral, hG, ↓reduceDIte, transpose_add_cbm, coe_add, transpose_eq_cbmApplyMeasure,
      ← setToFun_add_measure (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
        (dominatedFinMeasAdditive_cbmApplyMeasure μ C) hB hC]

Premises used: MeasureTheory.transpose_eq_cbmApplyMeasure, reduceDIte, MeasureTheory.VectorMeasure.coe_add, MeasureTheory.VectorMeasure.transpose_add_cbm, 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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : CompleteSpace G
⊢ sorry μ (fun (x : X) ↦ f x) (B + C) =
    HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)

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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : ¬CompleteSpace G
neg :
  sorry μ (fun (x : X) ↦ f x) (B + C) =
    HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)
⊢ ∫ᵛ (x : X), f x ∂[B + C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[C; μ]

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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
pos :
  ∀ (hG : CompleteSpace G),
    Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
neg :
  ∀ (hG : ¬CompleteSpace G),
    Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B 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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
hG : CompleteSpace G
pos : ∀ (hs : s.Nonempty), Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
neg : ∀ (hs : s = ∅), Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B 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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
hG : CompleteSpace G
hs : s.Nonempty
pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) (∑ i ∈ s, B i)) (∑ x ∈ s, sorry μ (fun (x : X) ↦ f x) (B x))
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B i; μ] (∑ i ∈ s, ∫ᵛ (x : X), f x ∂[B i; μ])

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

Premises used: MeasureTheory.VectorMeasure.coe_finsetSum, MeasureTheory.transpose_eq_cbmApplyMeasure, reduceDIte, MeasureTheory.VectorMeasure.transpose_finsetSum_cbm, 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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
hG : CompleteSpace G
hs : s.Nonempty
⊢ Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) (∑ i ∈ s, B i)) (∑ x ∈ s, sorry μ (fun (x : X) ↦ f x) (B x))

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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
hG : CompleteSpace G
hs : s = ∅
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B 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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
s : Finset ι
hf : ∀ i ∈ s, μ.Integrable f (B i)
hG : ¬CompleteSpace G
neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) (∑ i ∈ s, B i)) (∑ x ∈ s, sorry μ (fun (x : X) ↦ f x) (B x))
⊢ Eq.{u_5 + 1} (α := G) ∫ᵛ (x : X), f x ∂[∑ i ∈ s, B 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
-- 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 [integral, hG, ← setToFun_neg']

Premises used: MeasureTheory.setToFun_neg', 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
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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]
⊢ ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]

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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : CompleteSpace G
pos :
  sorry μ (fun (x : X) ↦ f x) (B - C) =
    HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)
⊢ ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]

Tactic:
simp only [integral, hG, ↓reduceDIte, transpose_sub_cbm, coe_sub,
      transpose_eq_cbmApplyMeasure, ← setToFun_sub_measure
        (dominatedFinMeasAdditive_cbmApplyMeasure μ B)
        (dominatedFinMeasAdditive_cbmApplyMeasure μ C) hB hC]

Premises used: MeasureTheory.VectorMeasure.transpose_sub_cbm, MeasureTheory.transpose_eq_cbmApplyMeasure, MeasureTheory.VectorMeasure.coe_sub, 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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : CompleteSpace G
⊢ sorry μ (fun (x : X) ↦ f x) (B - C) =
    HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)

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 C : E →L[ℝ] F →L[ℝ] G
hB : μ.Integrable f B
hC : μ.Integrable f C
hG : ¬CompleteSpace G
neg :
  sorry μ (fun (x : X) ↦ f x) (B - C) =
    HSub.hSub (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ f x) C)
⊢ ∫ᵛ (x : X), f x ∂[B - C; μ] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[C; μ]

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.VectorMeasure.integral
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ_1 ν μ : VectorMeasure X V
s : Set X
⊢ Eq (α := ℝ≥0∞) ((fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) ∅) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
⊢ Eq (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    ((preVariation (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) ⋯ ⋯ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
⊢ (↑μ.ennrealVariation : Set X → ℝ≥0∞) s = (μ.variation : (a : Set X) → ℝ≥0∞) s

Tactic:
Measure.toENNRealVectorMeasure_apply_measurable hs

Premises used: MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
⊢ let Q := Finpartition.ofPairwiseDisjoint P hP₂;
  Q = Finpartition.ofPairwiseDisjoint P hP₂

Tactic:
set Q := Finpartition.ofPairwiseDisjoint P hP₂ with defQ

Premises used: Finpartition.ofPairwiseDisjoint
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
⊢ let Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
    Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯;
  Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯

Tactic:
set Q' := Q.ofSubset (filter_subset MeasurableSet Q.parts) rfl with defQ'

Premises used: MeasurableSet, Finset.filter_subset, Finpartition.ofSubset, Finpartition.parts, rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
simp : ∀ (t : Set X), ¬t = ∅ → t ∈ P → MeasurableSet t → t ⊆ s
⊢ ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s

Tactic:
simp [Q', Q]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
⊢ ∀ (t : Set X), ¬t = ∅ → t ∈ P → MeasurableSet t → t ⊆ s

Tactic:
grind
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
⊢ ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s

Tactic:
have hQ' : ∀ t ∈ Q'.parts, t ⊆ s := by simp [Q', Q]; grind