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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s t : Set X
hs : MeasurableSet s
ht : MeasurableSet t
hdisj : Disjoint s t
x : E
⊢ Eq.{u_5 + 1} (α := G) ((cbmApplyMeasure μ B (s ∪ t) : (a : E) → G) x : G)
    ((cbmApplyMeasure μ B s + cbmApplyMeasure μ B t : (a : E) → G) x : G)

Tactic:
simp [of_union hdisj hs ht]

Premises used: MeasureTheory.VectorMeasure.of_union
-- 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
⊢ 0 ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖

Tactic:
positivity
-- 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
rw : ∀ (x : E), norm.{u_5} (E := G) ((cbmApplyMeasure μ B s : (a : E) → G) x : G) ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
⊢ ‖cbmApplyMeasure μ B s‖ ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖

Tactic:
rw [opNorm_le_iff (by positivity)]

Premises used: ContinuousLinearMap.opNorm_le_iff
-- 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
x : E
grw :
  norm.{u_5} (E := G) ((((B : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) ((↑μ : Set X → F) s) : G) ≤
    ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
grw₁ : ‖B‖ * ‖x‖ * ‖(↑μ : Set X → F) s‖ ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
grw₂ grw₃ : ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖ ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖
⊢ norm.{u_5} (E := G) ((cbmApplyMeasure μ B s : (a : E) → G) x : G) ≤ ‖B‖ * ‖(↑μ : Set X → F) s‖ * ‖x‖

Tactic:
grw [cbmApplyMeasure_apply, le_opNorm₂, mul_right_comm]

Premises used: ContinuousLinearMap.le_opNorm₂, mul_right_comm, MeasureTheory.cbmApplyMeasure_apply
-- 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
B : E →L[ℝ] F →L[ℝ] G
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose 0 B) 0

Tactic:
simp [transpose]

Premises used: MeasureTheory.VectorMeasure.transpose
-- 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
μ : VectorMeasure X F
h :
  ∀ (i : Set X),
    MeasurableSet i →
      ∀ (x : E),
        Eq.{u_5 + 1} (α := G) (((↑(μ.transpose 0) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
          (((↑0 : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose 0) 0

Tactic:
ext
-- 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
μ : VectorMeasure X F
i : Set X
h : MeasurableSet i
x : E
⊢ Eq.{u_5 + 1} (α := G) (((↑(μ.transpose 0) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
    (((↑0 : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)

Tactic:
simp [transpose]

Premises used: MeasureTheory.VectorMeasure.transpose
-- 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
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ (μ + ν).transpose B = μ.transpose B + ν.transpose B

Tactic:
simp [transpose]

Premises used: MeasureTheory.VectorMeasure.transpose
-- 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
μ : VectorMeasure X F
B C : E →L[ℝ] F →L[ℝ] G
h :
  ∀ (i : Set X),
    MeasurableSet i →
      ∀ (x : E),
        Eq.{u_5 + 1} (α := G) (((↑(μ.transpose (B + C)) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
          (((↑(μ.transpose B + μ.transpose C) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
⊢ μ.transpose (B + C) = μ.transpose B + μ.transpose C

Tactic:
ext
-- 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
μ : VectorMeasure X F
B C : E →L[ℝ] F →L[ℝ] G
i : Set X
h : MeasurableSet i
x : E
⊢ Eq.{u_5 + 1} (α := G) (((↑(μ.transpose (B + C)) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
    (((↑(μ.transpose B + μ.transpose C) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)

Tactic:
simp [transpose]

Premises used: MeasureTheory.VectorMeasure.transpose
-- 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
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ ∅, μ i) B) (∑ i ∈ ∅, (μ i).transpose B)

Tactic:
simp
-- 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
i : ι
s : Finset ι
his : i ∉ s
ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ insert i s, μ i) B) (∑ i ∈ insert i s, (μ i).transpose B)

Tactic:
simp [Finset.sum_insert, his, ih]

Premises used: Finset.sum_insert
-- 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 ι
empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ ∅, μ i) B) (∑ i ∈ ∅, (μ i).transpose B)
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)),
    Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ Insert.insert i s, μ i) B)
      (∑ i ∈ Insert.insert i s, (μ i).transpose B)
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]

Premises used: MeasureTheory.VectorMeasure.empty, Insert.insert, Finset.sum_insert
-- 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 ι
empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ ∅, μ i) B) (∑ i ∈ ∅, (μ i).transpose B)
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)),
    Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ Insert.insert i s, μ i) B)
      (∑ i ∈ Insert.insert i s, (μ i).transpose B)
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (transpose (∑ i ∈ s, μ i) B) (∑ i ∈ s, (μ i).transpose B)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]

Premises used: MeasureTheory.VectorMeasure.empty, Insert.insert, Finset.sum_insert
-- 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
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ ∅, B i)) (∑ i ∈ ∅, μ.transpose (B i))

Tactic:
simp
-- 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
i : ι
s : Finset ι
his : i ∉ s
ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ insert i s, B i)) (∑ i ∈ insert i s, μ.transpose (B i))

Tactic:
simp [Finset.sum_insert, his, ih]

Premises used: Finset.sum_insert
-- 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 ι
empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ ∅, B i)) (∑ i ∈ ∅, μ.transpose (B i))
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))),
    Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ Insert.insert i s, B i))
      (∑ i ∈ Insert.insert i s, μ.transpose (B i))
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]

Premises used: MeasureTheory.VectorMeasure.empty, Insert.insert, Finset.sum_insert
-- 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 ι
empty : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ ∅, B i)) (∑ i ∈ ∅, μ.transpose (B i))
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (ih : Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))),
    Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ Insert.insert i s, B i))
      (∑ i ∈ Insert.insert i s, μ.transpose (B i))
⊢ Eq (α := VectorMeasure X (E →L[ℝ] G)) (μ.transpose (∑ i ∈ s, B i)) (∑ i ∈ s, μ.transpose (B i))

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih => simp [Finset.sum_insert, his, ih]

Premises used: MeasureTheory.VectorMeasure.empty, Insert.insert, Finset.sum_insert
-- 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
h :
  ∀ (i : Set X),
    MeasurableSet i →
      ∀ (x : E),
        Eq.{u_5 + 1} (α := G) (((↑((-μ).transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
          (((↑(-μ.transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
⊢ (-μ).transpose B = -μ.transpose B

Tactic:
ext
-- 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
i : Set X
h : MeasurableSet i
x : E
⊢ Eq.{u_5 + 1} (α := G) (((↑((-μ).transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
    (((↑(-μ.transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)

Tactic:
simp [transpose]

Premises used: MeasureTheory.VectorMeasure.transpose
-- 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
h :
  ∀ (i : Set X),
    MeasurableSet i →
      ∀ (x : E),
        Eq.{u_5 + 1} (α := G) (((↑(μ.transpose (-B)) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
          (((↑(-μ.transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
⊢ μ.transpose (-B) = -μ.transpose B

Tactic:
ext
-- 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
i : Set X
h : MeasurableSet i
x : E
⊢ Eq.{u_5 + 1} (α := G) (((↑(μ.transpose (-B)) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
    (((↑(-μ.transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)

Tactic:
simp [transpose]

Premises used: MeasureTheory.VectorMeasure.transpose
-- 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
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
h :
  ∀ (i : Set X),
    MeasurableSet i →
      ∀ (x : E),
        Eq.{u_5 + 1} (α := G) (((↑((μ - ν).transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
          (((↑(μ.transpose B - ν.transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
⊢ (μ - ν).transpose B = μ.transpose B - ν.transpose B

Tactic:
ext
-- 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
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
i : Set X
h : MeasurableSet i
x : E
⊢ Eq.{u_5 + 1} (α := G) (((↑((μ - ν).transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
    (((↑(μ.transpose B - ν.transpose B) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)

Tactic:
simp [transpose]

Premises used: MeasureTheory.VectorMeasure.transpose
-- 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
μ : VectorMeasure X F
B C : E →L[ℝ] F →L[ℝ] G
h :
  ∀ (i : Set X),
    MeasurableSet i →
      ∀ (x : E),
        Eq.{u_5 + 1} (α := G) (((↑(μ.transpose (B - C)) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
          (((↑(μ.transpose B - μ.transpose C) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
⊢ μ.transpose (B - C) = μ.transpose B - μ.transpose C

Tactic:
ext
-- 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
μ : VectorMeasure X F
B C : E →L[ℝ] F →L[ℝ] G
i : Set X
h : MeasurableSet i
x : E
⊢ Eq.{u_5 + 1} (α := G) (((↑(μ.transpose (B - C)) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)
    (((↑(μ.transpose B - μ.transpose C) : Set X → E →L[ℝ] G) i : (a : E) → G) x : G)

Tactic:
simp [transpose]

Premises used: MeasureTheory.VectorMeasure.transpose
-- 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
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ] = 0
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), f x ∂[B; μ] = 0
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = 0

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
hG : CompleteSpace G
pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) B) 0
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = 0

Tactic:
simp [integral, setToFun_undef _ h]

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
hG : ¬CompleteSpace G
neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ f x) B) 0
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = 0

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
pos : ∀ (hG : CompleteSpace G), ∫ᵛ (x : X), 0 ∂[B; μ] = 0
neg : ∀ (hG : ¬CompleteSpace G), ∫ᵛ (x : X), 0 ∂[B; μ] = 0
⊢ ∫ᵛ (x : X), 0 ∂[B; μ] = 0

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hG : CompleteSpace G
pos : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ 0) B) 0
⊢ ∫ᵛ (x : X), 0 ∂[B; μ] = 0

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hG : CompleteSpace G
⊢ Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ 0) B) 0

Tactic:
setToFun_zero (dominatedFinMeasAdditive_cbmApplyMeasure μ B)

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, MeasureTheory.setToFun_zero, 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hG : ¬CompleteSpace G
neg : Eq.{u_5 + 1} (α := G) (sorry μ (fun (x : X) ↦ 0) B) 0
⊢ ∫ᵛ (x : X), 0 ∂[B; μ] = 0

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
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 =
    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 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 =
    HAdd.hAdd (α := G) (sorry μ (fun (x : X) ↦ f x) B) (sorry μ (fun (x : X) ↦ g x) B)

Tactic:
setToFun_add (dominatedFinMeasAdditive_cbmApplyMeasure μ B) hf hg

Premises used: Unit.unit, sorryAx, MeasureTheory.setToFun_add, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat