awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
pos : ∀ (hxu' : x ∈ uᶜ), x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
neg : ∀ (hxu' : x ∉ uᶜ), x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
by_cases hxu' : x ∈ uᶜ
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
Or.inl ⟨hxu', hx⟩

Premises used: Set.union, Set.Mem, setOf, And.intro, Or.inl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
exact Or.inl ⟨hxu', hx⟩

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∉ uᶜ
neg : ∀ (hxu : x ∈ uᶜ), x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
neg₁ : ∀ (hxv : x ∈ vᶜ), x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
rcases ht hx with (hxu | hxv)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∉ uᶜ
hxu : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
False.elim (hxu' hxu)

Premises used: False.elim
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∉ uᶜ
hxv : x ∈ vᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
Or.inr ⟨⟨hxv, hxu'⟩, hx⟩

Premises used: Set.union, Set.Mem, setOf, And.intro, Or.inr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ t
hxu' : x ∉ uᶜ
hxu : x ∈ uᶜ
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
exacts [False.elim (hxu' hxu), Or.inr ⟨⟨hxv, hxu'⟩, hx⟩]

Premises used: False.elim, Or.inr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
h₂ : ∀ (hx : x ∈ uᶜ ∩ t), x ∈ t
h₃ : ∀ (hx : x ∈ vᶜ \ uᶜ ∩ t), x ∈ t
⊢ x ∈ t

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ uᶜ ∩ t
⊢ x ∈ t

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ uᶜ ∩ t
⊢ x ∈ t

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ vᶜ \ uᶜ ∩ t
⊢ x ∈ t

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0
hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
x : α
hx : x ∈ vᶜ \ uᶜ ∩ t
⊢ x ∈ t

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w₁ w₂ : VectorMeasure α N
inst_4 : T2Space M
inst_5 : ContinuousAdd N
h₁ : v ⟂ᵥ w₁
h₂ : v ⟂ᵥ w₂
⊢ v ⟂ᵥ w₁ + w₂

Tactic:
(add_left h₁.symm h₂.symm).symm

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.add_left, MeasureTheory.VectorMeasure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
R : Type u_6
inst_4 : Semiring R
inst_5 : DistribMulAction R N
inst_6 : ContinuousConstSMul R N
r : R
h : v ⟂ᵥ w
s : Set α
hmeas : MeasurableSet s
hs₁ : ∀ t ⊆ s, (↑v : Set α → M) t = 0
hs₂ : ∀ t ⊆ sᶜ, (↑w : Set α → N) t = 0
t : Set α
ht : t ⊆ sᶜ
⊢ (↑(r • w) : Set α → N) t = 0

Tactic:
simp only [coe_smul, Pi.smul_apply, hs₂ t ht, smul_zero]

Premises used: MeasureTheory.VectorMeasure.coe_smul, smul_zero, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid N
inst_3 : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
R : Type u_6
inst_4 : Semiring R
inst_5 : DistribMulAction R M
inst_6 : ContinuousConstSMul R M
r : R
h : v ⟂ᵥ w
⊢ r • v ⟂ᵥ w

Tactic:
(smul_right r h.symm).symm

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.smul_right, MeasureTheory.VectorMeasure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
h : v ⟂ᵥ w
obtain :
  ∀ (u : Set α) (hmu : MeasurableSet u) (hu₁ : ∀ t ⊆ u, (↑v : Set α → M) t = 0)
    (hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0), -v ⟂ᵥ w
⊢ -v ⟂ᵥ w

Tactic:
obtain ⟨u, hmu, hu₁, hu₂⟩ := h
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
⊢ -v ⟂ᵥ w

Tactic:
⟨u, hmu, fun s hs => ?_, hu₂⟩

Premises used: And.intro, Exists.intro, MeasureTheory.VectorMeasure.MutuallySingular
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
refine : ∀ (s : Set α) (hs : s ⊆ u), (↑(-v) : Set α → M) s = 0
⊢ -v ⟂ᵥ w

Tactic:
refine ⟨u, hmu, fun s hs => ?_, hu₂⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
s : Set α
hs : s ⊆ u
rw : (↑v : Set α → M) s = 0
⊢ (↑(-v) : Set α → M) s = 0

Tactic:
rw [neg_apply v s, neg_eq_zero]

Premises used: MeasureTheory.VectorMeasure.neg_apply, neg_eq_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
s : Set α
hs : s ⊆ u
⊢ (↑v : Set α → M) s = 0

Tactic:
hu₁ s hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
s : Set α
hs : s ⊆ u
⊢ (↑v : Set α → M) s = 0

Tactic:
exact hu₁ s hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
N : Type u_6
inst_2 : AddCommGroup N
inst_3 : TopologicalSpace N
inst_4 : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ⟂ᵥ w
⊢ v ⟂ᵥ -w

Tactic:
h.symm.neg_left.symm

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.neg_left, MeasureTheory.VectorMeasure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst : AddCommMonoid N
inst_1 : TopologicalSpace N
M : Type u_6
inst_2 : AddCommGroup M
inst_3 : TopologicalSpace M
inst_4 : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
⊢ -v ⟂ᵥ w ↔ v ⟂ᵥ w

Tactic:
⟨fun h => neg_neg v ▸ h.neg_left, neg_left⟩

Premises used: Eq.rec, neg_neg, MeasureTheory.VectorMeasure.MutuallySingular.neg_left, Iff.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
N : Type u_6
inst_2 : AddCommGroup N
inst_3 : TopologicalSpace N
inst_4 : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
⊢ v ⟂ᵥ -w ↔ v ⟂ᵥ w

Tactic:
⟨fun h => neg_neg w ▸ h.neg_right, neg_right⟩

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.neg_right, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
rw : (↑v : Set α → M) ∅ = 0
rw₁ rw₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ (if MeasurableSet.{u_1} (α := α) ∅ then (↑v : Set α → M) ∅ else 0) = 0

Tactic:
rw [if_pos (@MeasurableSet.empty _ m), v.empty]

Premises used: MeasureTheory.VectorMeasure.empty, MeasurableSet.empty, if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : ¬MeasurableSet i
rw rw₁ : Eq.{u_4 + 1} (α := M) 0 0
⊢ (if MeasurableSet i then (↑v : Set α → M) i else 0) = 0

Tactic:
rw [if_neg hi]

Premises used: if_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ∀ (k : ℕ), MeasurableSet (f k)

Tactic:
have hf₁' : ∀ k, MeasurableSet[n] (f k) := fun k => hle _ (hf₁ k)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
⊢ HasSum (fun (i : ℕ) ↦ (↑v : Set α → M) (f i)) ((↑v : Set α → M) (⋃ (i : ℕ), f i))

Tactic:
v.m_iUnion hf₁' hf₂

Premises used: MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
h :
  Eq.{u_4 + 1} (α := ℕ → M) (fun (i : ℕ) ↦ if MeasurableSet (f i) then (↑v : Set α → M) (f i) else 0) fun (i : ℕ) ↦
    (↑v : Set α → M) (f i)
h₁ :
  (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) (⋃ (i : ℕ), f i) else 0) =
    (↑v : Set α → M) (⋃ (i : ℕ), f i)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) then (↑v : Set α → M) (f i) else 0)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) (⋃ (i : ℕ), f i) else 0)

Tactic:
convert! v.m_iUnion hf₁' hf₂ using 1

Premises used: MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
h : ∀ (n_1 : ℕ), (if MeasurableSet (f n_1) then (↑v : Set α → M) (f n_1) else 0) = (↑v : Set α → M) (f n_1)
⊢ Eq.{u_4 + 1} (α := ℕ → M) (fun (i : ℕ) ↦ if MeasurableSet (f i) then (↑v : Set α → M) (f i) else 0) fun (i : ℕ) ↦
    (↑v : Set α → M) (f i)

Tactic:
ext n
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n_1 : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n_1
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
n : ℕ
h h₁ : (↑v : Set α → M) (f n) = (↑v : Set α → M) (f n)
⊢ (if MeasurableSet (f n) then (↑v : Set α → M) (f n) else 0) = (↑v : Set α → M) (f n)

Tactic:
rw [if_pos (hf₁ n)]

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
h h₁ : (↑v : Set α → M) (⋃ (i : ℕ), f i) = (↑v : Set α → M) (⋃ (i : ℕ), f i)
⊢ (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) (⋃ (i : ℕ), f i) else 0) =
    (↑v : Set α → M) (⋃ (i : ℕ), f i)

Tactic:
rw [if_pos (@MeasurableSet.iUnion _ _ m _ _ hf₁)]

Premises used: if_pos, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
h : ∀ (i : Set α) (hi : MeasurableSet i), (↑(v.trim ⋯) : Set α → M) i = (↑v : Set α → M) i
⊢ v.trim ⋯ = v

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (↑(v.trim ⋯) : Set α → M) i = (↑v : Set α → M) i

Tactic:
if_pos hi

Premises used: if_pos, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (↑(v.trim ⋯) : Set α → M) i = (↑v : Set α → M) i

Tactic:
exact if_pos hi

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
hle : m ≤ n
h : ∀ (i : Set α) (hi : MeasurableSet i), Eq.{u_4 + 1} (α := M) ((↑(trim 0 hle) : Set α → M) i) ((↑0 : Set α → M) i)
⊢ Eq (α := VectorMeasure α M) (trim 0 hle) 0

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
hle : m ≤ n
i : Set α
hi : MeasurableSet i
⊢ Eq.{u_4 + 1} (α := M) ((↑(trim 0 hle) : Set α → M) i) ((↑0 : Set α → M) i)

Tactic:
if_pos hi

Premises used: if_pos, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
hle : m ≤ n
i : Set α
hi : MeasurableSet i
⊢ Eq.{u_4 + 1} (α := M) ((↑(trim 0 hle) : Set α → M) i) ((↑0 : Set α → M) i)

Tactic:
exact if_pos hi

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
⊢ (↑(v.trim hle) : Set α → M) i = (↑v : Set α → M) i

Tactic:
if_pos hi

Premises used: if_pos, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
h :
  ∀ (j : Set α) (hj : MeasurableSet j),
    (↑((v.trim hle).restrict i) : Set α → M) j = (↑((v.restrict i).trim hle) : Set α → M) j
⊢ (v.trim hle).restrict i = (v.restrict i).trim hle

Tactic:
ext j hj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
h : MeasurableSet (j ∩ i)
h₁ : MeasurableSet i
h₂ : MeasurableSet j
h₃ : MeasurableSet i
h₄ : MeasurableSet j
⊢ (↑((v.trim hle).restrict i) : Set α → M) j = (↑((v.restrict i).trim hle) : Set α → M) j

Tactic:
rw [@restrict_apply _ m, trim_measurableSet_eq hle hj, restrict_apply, trim_measurableSet_eq]

Premises used: MeasureTheory.VectorMeasure.trim_measurableSet_eq, MeasureTheory.VectorMeasure.restrict_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet (j ∩ i)

Tactic:
measurability