awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
pos :
  ∀ (i : Set β) (hi : MeasurableSet i),
    (↑((v + w).map f) : Set β → M) i = (↑(HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)) : Set β → M) i
⊢ (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ (↑((v + w).map f) : Set β → M) i = (↑(HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)) : Set β → M) i

Tactic:
simp [map_apply _ hf hi]

Premises used: MeasureTheory.VectorMeasure.map_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)

Tactic:
simp [map, dif_neg hf]

Premises used: dif_neg, MeasureTheory.VectorMeasure.map
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
pos : ∀ (hi : MeasurableSet i), (v + w).restrict i = v.restrict i + w.restrict i
neg : ∀ (hi : ¬MeasurableSet i), (v + w).restrict i = v.restrict i + w.restrict i
⊢ (v + w).restrict i = v.restrict i + w.restrict i

Tactic:
by_cases hi : MeasurableSet i

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
pos :
  ∀ (j : Set α) (hj : MeasurableSet j),
    (↑((v + w).restrict i) : Set α → M) j = (↑(v.restrict i + w.restrict i) : Set α → M) j
⊢ (v + w).restrict i = v.restrict i + w.restrict i

Tactic:
ext j hj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (↑((v + w).restrict i) : Set α → M) j = (↑(v.restrict i + w.restrict i) : Set α → M) j

Tactic:
simp [restrict_apply _ hi hj]

Premises used: MeasureTheory.VectorMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (v + w).restrict i = v.restrict i + w.restrict i

Tactic:
simp [restrict_not_measurable _ hi]

Premises used: MeasureTheory.VectorMeasure.restrict_not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : T2Space M
inst_4 : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : ∀ (A : Set α) (hA : MeasurableSet A), (↑(v.restrict i + v.restrict iᶜ) : Set α → M) A = (↑v : Set α → M) A
⊢ v.restrict i + v.restrict iᶜ = v

Tactic:
ext A hA
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : T2Space M
inst_4 : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
h : (↑v : Set α → M) (A ∩ i ∪ A ∩ iᶜ) = (↑v : Set α → M) A
rw : Disjoint (A ∩ i) (A ∩ iᶜ)
⊢ (↑(v.restrict i + v.restrict iᶜ) : Set α → M) A = (↑v : Set α → M) A

Tactic:
rw [add_apply, restrict_apply _ hi hA, restrict_apply _ hi.compl hA,
    ← of_union _ (hA.inter hi) (hA.inter hi.compl)]

Premises used: MeasureTheory.VectorMeasure.restrict_apply, MeasureTheory.VectorMeasure.of_union, MeasurableSet.compl, MeasureTheory.VectorMeasure.add_apply, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : T2Space M
inst_4 : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
⊢ (↑v : Set α → M) (A ∩ i ∪ A ∩ iᶜ) = (↑v : Set α → M) A

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : T2Space M
inst_4 : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
⊢ Disjoint (A ∩ i) (A ∩ iᶜ)

Tactic:
disjoint_compl_right.inter_right' A |>.inter_left' A

Premises used: Disjoint.inter_left', disjoint_compl_right, Disjoint.inter_right'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : T2Space M
inst_4 : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
⊢ Disjoint (A ∩ i) (A ∩ iᶜ)

Tactic:
exact disjoint_compl_right.inter_right' A |>.inter_left' A

Premises used: Disjoint.inter_left', disjoint_compl_right, Disjoint.inter_right'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
pos : ∀ (hi : MeasurableSet i), (-v).restrict i = -v.restrict i
neg : ∀ (hi : ¬MeasurableSet i), (-v).restrict i = -v.restrict i
⊢ (-v).restrict i = -v.restrict i

Tactic:
by_cases hi : MeasurableSet i

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
pos : ∀ (j : Set α) (hj : MeasurableSet j), (↑((-v).restrict i) : Set α → M) j = (↑(-v.restrict i) : Set α → M) j
⊢ (-v).restrict i = -v.restrict i

Tactic:
ext j hj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (↑((-v).restrict i) : Set α → M) j = (↑(-v.restrict i) : Set α → M) j

Tactic:
simp [restrict_apply _ hi hj]

Premises used: MeasureTheory.VectorMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ (-v).restrict i = -v.restrict i

Tactic:
simp [restrict_not_measurable _ hi]

Premises used: MeasureTheory.VectorMeasure.restrict_not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
⊢ (v - w).restrict i = v.restrict i - w.restrict i

Tactic:
simp [sub_eq_add_neg, restrict_add, restrict_neg]

Premises used: MeasureTheory.VectorMeasure.restrict_add, sub_eq_add_neg, MeasureTheory.VectorMeasure.restrict_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
pos : ∀ (hf : Measurable f), (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)
neg : ∀ (hf : ¬Measurable f), (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)
⊢ (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)

Tactic:
by_cases hf : Measurable f

Premises used: Measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
pos :
  ∀ (i : Set β) (hi : MeasurableSet i),
    (↑((c • v).map f) : Set β → M) i = (↑(HSMul.hSMul (β := VectorMeasure β M) c (v.map f)) : Set β → M) i
⊢ (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ (↑((c • v).map f) : Set β → M) i = (↑(HSMul.hSMul (β := VectorMeasure β M) c (v.map f)) : Set β → M) i

Tactic:
simp [map_apply _ hf hi]

Premises used: MeasureTheory.VectorMeasure.map_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
neg : 0 = HSMul.hSMul (β := VectorMeasure β M) c 0
⊢ (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)

Tactic:
simp only [map, dif_neg hf]

Premises used: dif_neg, MeasureTheory.VectorMeasure.map
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
neg : ∀ (i : Set β), MeasurableSet i → (↑0 : Set β → M) i = (↑(HSMul.hSMul (β := VectorMeasure β M) c 0) : Set β → M) i
⊢ 0 = HSMul.hSMul (β := VectorMeasure β M) c 0

Tactic:
ext i
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
i : Set β
h : MeasurableSet i
⊢ (↑0 : Set β → M) i = (↑(HSMul.hSMul (β := VectorMeasure β M) c 0) : Set β → M) i

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
pos : ∀ (hi : MeasurableSet i), (c • v).restrict i = c • v.restrict i
neg : ∀ (hi : ¬MeasurableSet i), (c • v).restrict i = c • v.restrict i
⊢ (c • v).restrict i = c • v.restrict i

Tactic:
by_cases hi : MeasurableSet i

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
pos : ∀ (j : Set α) (hj : MeasurableSet j), (↑((c • v).restrict i) : Set α → M) j = (↑(c • v.restrict i) : Set α → M) j
⊢ (c • v).restrict i = c • v.restrict i

Tactic:
ext j hj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (↑((c • v).restrict i) : Set α → M) j = (↑(c • v.restrict i) : Set α → M) j

Tactic:
simp [restrict_apply _ hi hj]

Premises used: MeasureTheory.VectorMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
neg : 0 = HSMul.hSMul (β := VectorMeasure α M) c 0
⊢ (c • v).restrict i = c • v.restrict i

Tactic:
simp only [restrict_not_measurable _ hi]

Premises used: MeasureTheory.VectorMeasure.restrict_not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
neg : ∀ (j : Set α), MeasurableSet j → (↑0 : Set α → M) j = (↑(HSMul.hSMul (β := VectorMeasure α M) c 0) : Set α → M) j
⊢ 0 = HSMul.hSMul (β := VectorMeasure α M) c 0

Tactic:
ext j
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
hi : ¬MeasurableSet i
j : Set α
h : MeasurableSet j
⊢ (↑0 : Set α → M) j = (↑(HSMul.hSMul (β := VectorMeasure α M) c 0) : Set α → M) j

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤ w ↔ ∀ (i : Set α), MeasurableSet i → (↑v : Set α → M) i ≤ (↑w : Set α → M) i

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤ w ↔ ∀ (i : Set α), (↑v : Set α → M) i ≤ (↑w : Set α → M) i

Tactic:
⟨fun h i => ?_, fun h i _ => h i⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
refine : ∀ (h : v ≤ w) (i : Set α), (↑v : Set α → M) i ≤ (↑w : Set α → M) i
⊢ v ≤ w ↔ ∀ (i : Set α), (↑v : Set α → M) i ≤ (↑w : Set α → M) i

Tactic:
refine ⟨fun h i => ?_, fun h i _ => h i⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
pos : ∀ (hi : MeasurableSet i), (↑v : Set α → M) i ≤ (↑w : Set α → M) i
neg : ∀ (hi : ¬MeasurableSet i), (↑v : Set α → M) i ≤ (↑w : Set α → M) i
⊢ (↑v : Set α → M) i ≤ (↑w : Set α → M) i

Tactic:
by_cases hi : MeasurableSet i

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : MeasurableSet i
⊢ (↑v : Set α → M) i ≤ (↑w : Set α → M) i

Tactic:
h i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : MeasurableSet i
⊢ (↑v : Set α → M) i ≤ (↑w : Set α → M) i

Tactic:
exact h i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
h : v ≤ w
i : Set α
hi : ¬MeasurableSet i
neg : 0 ≤ (↑w : Set α → M) i
neg₁ neg₂ : LE.le.{u_3} (α := M) 0 0
⊢ (↑v : Set α → M) i ≤ (↑w : Set α → M) i

Tactic:
rw [v.not_measurable hi, w.not_measurable hi]

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ v ≤[i] w ↔ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑w : Set α → M) j

Tactic:
⟨fun h j hj₁ hj₂ => restrict_eq_self v hi hj₁ hj₂ ▸ restrict_eq_self w hi hj₁ hj₂ ▸ h j hj₁,
    fun h => le_iff.1 fun _ hj =>
      (restrict_apply v hi hj).symm ▸ (restrict_apply w hi hj).symm ▸
      h (hj.inter hi) Set.inter_subset_right⟩

Premises used: MeasureTheory.VectorMeasure.restrict_eq_self, MeasureTheory.VectorMeasure.restrict_apply, Eq.rec, MeasureTheory.VectorMeasure.le_iff, Iff.intro, Iff.mp, Eq.symm, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
pos : ∀ (hj₁ : MeasurableSet j), (↑v : Set α → M) j ≤ (↑w : Set α → M) j
neg : ∀ (hj₁ : ¬MeasurableSet j), (↑v : Set α → M) j ≤ (↑w : Set α → M) j
⊢ (↑v : Set α → M) j ≤ (↑w : Set α → M) j

Tactic:
by_cases hj₁ : MeasurableSet j

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : MeasurableSet j
⊢ (↑v : Set α → M) j ≤ (↑w : Set α → M) j

Tactic:
(restrict_le_restrict_iff _ _ hi).1 hi₂ hj₁ hj

Premises used: Iff.mp, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : MeasurableSet j
⊢ (↑v : Set α → M) j ≤ (↑w : Set α → M) j

Tactic:
exact (restrict_le_restrict_iff _ _ hi).1 hi₂ hj₁ hj

Premises used: Iff.mp, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
neg : 0 ≤ (↑w : Set α → M) j
neg₁ neg₂ : LE.le.{u_3} (α := M) 0 0
⊢ (↑v : Set α → M) j ≤ (↑w : Set α → M) j

Tactic:
rw [v.not_measurable hj₁, w.not_measurable hj₁]

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑w : Set α → M) j
pos : ∀ (hi : MeasurableSet i), v ≤[i] w
neg : ∀ (hi : ¬MeasurableSet i), v ≤[i] w
⊢ v ≤[i] w

Tactic:
by_cases hi : MeasurableSet i

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑w : Set α → M) j
hi : MeasurableSet i
⊢ v ≤[i] w

Tactic:
(restrict_le_restrict_iff _ _ hi).2 h

Premises used: Iff.mpr, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑w : Set α → M) j
hi : MeasurableSet i
⊢ v ≤[i] w

Tactic:
exact (restrict_le_restrict_iff _ _ hi).2 h

Premises used: Iff.mpr, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑w : Set α → M) j
hi : ¬MeasurableSet i
neg : 0 ≤ w.restrict i
neg₁ neg₂ : LE.le (α := VectorMeasure α M) 0 0
⊢ v ≤[i] w

Tactic:
rw [restrict_not_measurable v hi, restrict_not_measurable w hi]

Premises used: MeasureTheory.VectorMeasure.restrict_not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hij : j ⊆ i
⊢ v ≤[j] w

Tactic:
restrict_le_restrict_of_subset_le v w fun _ _ hk₂ =>
    subset_le_of_restrict_le_restrict v w hi₁ hi₂ (Set.Subset.trans hk₂ hij)

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le, Set.Subset.trans, MeasureTheory.VectorMeasure.subset_le_of_restrict_le_restrict
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤[∅] w

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v w : VectorMeasure α M
⊢ v ≤[univ] w ↔ v ≤ w

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommGroup M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
rw : -(↑w : Set α → M) (j ∩ i) ≤ -(↑v : Set α → M) (j ∩ i)
⊢ (↑((-w).restrict i) : Set α → M) j ≤ (↑((-v).restrict i) : Set α → M) j

Tactic:
rw [restrict_apply _ hi hj₁, restrict_apply _ hi hj₁, neg_apply, neg_apply]

Premises used: MeasureTheory.VectorMeasure.neg_apply, MeasureTheory.VectorMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommGroup M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ -(↑w : Set α → M) (j ∩ i) ≤ -(↑v : Set α → M) (j ∩ i)

Tactic:
neg_le_neg ?_

Premises used: neg_le_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommGroup M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
refine : (↑v : Set α → M) (j ∩ i) ≤ (↑w : Set α → M) (j ∩ i)
⊢ -(↑w : Set α → M) (j ∩ i) ≤ -(↑v : Set α → M) (j ∩ i)

Tactic:
refine neg_le_neg ?_

Premises used: MeasureTheory.VectorMeasure.neg_le_neg