awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h :
  ∀ ⦃s : Set α⦄, Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0
mp :
  ∀ (s : Set α) (hmeas : MeasurableSet s) (hs : (↑μ : Set α → ℝ≥0∞) s = 0),
    Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ v ≪ᵥ μ

Tactic:
refine mk fun s hmeas hs => h ?_

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h :
  ∀ ⦃s : Set α⦄, Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0
s : Set α
hmeas : MeasurableSet s
hs : (↑μ : Set α → ℝ≥0∞) s = 0
mp : (μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
mp₁ mp₂ : (↑μ : Set α → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← hs, ennrealToMeasure_apply hmeas]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos : ∀ (hmeas : MeasurableSet s), (↑v : Set α → M) s = 0
neg : ∀ (hmeas : ¬MeasurableSet s), (↑v : Set α → M) s = 0
⊢ (↑v : Set α → M) s = 0

Tactic:
by_cases hmeas : MeasurableSet s

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hmeas : MeasurableSet s
⊢ (↑μ : Set α → ℝ≥0∞) s = 0

Tactic:
rw [ennrealToMeasure_apply hmeas] at hs

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hmeas : MeasurableSet s
hs₁ : (↑μ : Set α → ℝ≥0∞) s = 0
⊢ MeasurableSet s

Tactic:
rw [ennrealToMeasure_apply hmeas] at hs

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : (↑μ : Set α → ℝ≥0∞) s = 0
hmeas : MeasurableSet s
⊢ (↑v : Set α → M) s = 0

Tactic:
h hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : (↑μ : Set α → ℝ≥0∞) s = 0
hmeas : MeasurableSet s
⊢ (↑v : Set α → M) s = 0

Tactic:
exact h hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hmeas : ¬MeasurableSet s
⊢ (↑v : Set α → M) s = 0

Tactic:
not_measurable v hmeas

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hmeas : ¬MeasurableSet s
⊢ (↑v : Set α → M) s = 0

Tactic:
exact not_measurable v hmeas

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
⊢ v ⟂ᵥ w

Tactic:
⟨s, hs, fun t hst => ?_, fun t hst => ?_⟩

Premises used: And.intro, Exists.intro, MeasureTheory.VectorMeasure.MutuallySingular
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
refine_1 : ∀ (t : Set α) (hst : t ⊆ s), (↑v : Set α → M) t = 0
refine_2 : ∀ (t : Set α) (hst : t ⊆ sᶜ), (↑w : Set α → N) t = 0
⊢ v ⟂ᵥ w

Tactic:
refine ⟨s, hs, fun t hst => ?_, fun t hst => ?_⟩
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ s
pos : ∀ (ht : MeasurableSet t), (↑v : Set α → M) t = 0
neg : ∀ (ht : ¬MeasurableSet t), (↑v : Set α → M) t = 0
⊢ (↑v : Set α → M) t = 0

Tactic:
by_cases ht : MeasurableSet t

Premises used: MeasurableSet
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ sᶜ
pos : ∀ (ht : MeasurableSet t), (↑w : Set α → N) t = 0
neg : ∀ (ht : ¬MeasurableSet t), (↑w : Set α → N) t = 0
⊢ (↑w : Set α → N) t = 0

Tactic:
by_cases ht : MeasurableSet t

Premises used: MeasurableSet
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ s
ht : MeasurableSet t
⊢ (↑v : Set α → M) t = 0

Tactic:
h₁ t hst ht
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ s
ht : MeasurableSet t
⊢ (↑v : Set α → M) t = 0

Tactic:
exact h₁ t hst ht
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ s
ht : ¬MeasurableSet t
⊢ (↑v : Set α → M) t = 0

Tactic:
not_measurable v ht

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ s
ht : ¬MeasurableSet t
⊢ (↑v : Set α → M) t = 0

Tactic:
exact not_measurable v ht

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ sᶜ
ht : MeasurableSet t
⊢ (↑w : Set α → N) t = 0

Tactic:
h₂ t hst ht
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ sᶜ
ht : MeasurableSet t
⊢ (↑w : Set α → N) t = 0

Tactic:
exact h₂ t hst ht
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ sᶜ
ht : ¬MeasurableSet t
⊢ (↑w : Set α → N) t = 0

Tactic:
not_measurable w ht

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- 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
s : Set α
hs : MeasurableSet s
h₁ : ∀ t ⊆ s, MeasurableSet t → (↑v : Set α → M) t = 0
h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → (↑w : Set α → N) t = 0
t : Set α
hst : t ⊆ sᶜ
ht : ¬MeasurableSet t
⊢ (↑w : Set α → N) t = 0

Tactic:
exact not_measurable w ht

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- 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
h : v ⟂ᵥ w
⊢ w ⟂ᵥ v

Tactic:
let ⟨s, hmeas, hs₁, hs₂⟩ := h
  ⟨sᶜ, hmeas.compl, hs₂, fun t ht => hs₁ _ (compl_compl s ▸ ht : t ⊆ s)⟩

Premises used: compl_compl, Compl.compl, Eq.rec, MeasurableSet.compl, _private.0.MeasureTheory.VectorMeasure.MutuallySingular.symm.match_1, And.intro, Exists.intro, MeasureTheory.VectorMeasure.MutuallySingular
-- 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
⊢ MutuallySingular.{u_1, u_4, u_5} (N := N) v 0

Tactic:
⟨∅, MeasurableSet.empty, fun _ ht => (Set.subset_empty_iff.1 ht).symm ▸ v.empty,
    fun _ _ => zero_apply _⟩

Premises used: MeasureTheory.VectorMeasure.empty, MeasurableSet.empty, MeasureTheory.VectorMeasure.zero_apply, Eq.rec, And.intro, Exists.intro, Iff.mp, Set.subset_empty_iff, EmptyCollection.emptyCollection, Eq.symm, MeasureTheory.VectorMeasure.MutuallySingular
-- 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
w : VectorMeasure α N
⊢ MutuallySingular.{u_1, u_4, u_5} (M := M) 0 w

Tactic:
zero_right.symm

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.zero_right, 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₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst_4 : T2Space N
inst_5 : ContinuousAdd M
h₁ : v₁ ⟂ᵥ w
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₁ + v₂ ⟂ᵥ w
⊢ v₁ + v₂ ⟂ᵥ w

Tactic:
obtain ⟨u, hmu, hu₁, hu₂⟩ := h₁
-- 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
h₂ : v₂ ⟂ᵥ w
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑v₁ : Set α → M) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0
obtain :
  ∀ (v : Set α) (hmv : MeasurableSet v) (hv₁ : ∀ t ⊆ v, (↑v₂ : Set α → M) t = 0)
    (hv₂ : ∀ t ⊆ vᶜ, (↑w : Set α → N) t = 0), v₁ + v₂ ⟂ᵥ w
⊢ v₁ + v₂ ⟂ᵥ w

Tactic:
obtain ⟨v, hmv, hv₁, hv₂⟩ := h₂
-- 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
⊢ v₁ + v₂ ⟂ᵥ w

Tactic:
mk (u ∩ v) (hmu.inter hmv) (fun t ht _ => ?_) fun t ht hmt => ?_

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.mk, Inter.inter, MeasurableSet.inter
-- 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
refine_1 : ∀ (t : Set α) (ht : t ⊆ u ∩ v), MeasurableSet t → (↑(v₁ + v₂) : Set α → M) t = 0
refine_2 : ∀ (t : Set α) (ht : t ⊆ (u ∩ v)ᶜ) (hmt : MeasurableSet t), (↑w : Set α → N) t = 0
⊢ v₁ + v₂ ⟂ᵥ w

Tactic:
refine mk (u ∩ v) (hmu.inter hmv) (fun t ht _ => ?_) fun t ht hmt => ?_

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.mk, Inter.inter, MeasurableSet.inter
-- 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
h : MeasurableSet t
refine_1 : (↑v₁ : Set α → M) t + (↑v₂ : Set α → M) t = 0
refine_1₁ : 0 + (↑v₂ : Set α → M) t = 0
refine_1₂ : HAdd.hAdd (α := M) 0 0 = 0
refine_1₃ refine_1₄ : Eq.{u_4 + 1} (α := M) 0 0
⊢ (↑(v₁ + v₂) : Set α → M) t = 0

Tactic:
rw [add_apply, hu₁ _ (Set.subset_inter_iff.1 ht).1, hv₁ _ (Set.subset_inter_iff.1 ht).2,
      zero_add]

Premises used: Set.subset_inter_iff, zero_add, And.right, And.left, Iff.mp, MeasureTheory.VectorMeasure.add_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₁ 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
⊢ t ⊆ uᶜ ∪ vᶜ

Tactic:
rw [Set.compl_inter] at ht

Premises used: Set.compl_inter
-- 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
ht₁ : t ⊆ uᶜ ∪ vᶜ
⊢ MeasurableSet t

Tactic:
rw [Set.compl_inter] at ht

Premises used: Set.compl_inter
-- 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
refine_2 : vᶜ \ uᶜ ∩ t ⊆ vᶜ
refine_2₁ : uᶜ ∩ t ⊆ uᶜ
rw : Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)
rw₁ : t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
⊢ (↑w : Set α → N) t = 0

Tactic:
rw [(_ : t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t),
      of_union _ (hmu.compl.inter hmt) ((hmv.compl.diff hmu.compl).inter hmt), hu₂, hv₂, add_zero]

Premises used: MeasurableSet.diff, MeasureTheory.VectorMeasure.of_union, MeasurableSet.compl, add_zero, MeasurableSet.inter
-- 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
⊢ vᶜ \ uᶜ ∩ t ⊆ vᶜ

Tactic:
Set.Subset.trans Set.inter_subset_left diff_subset

Premises used: Set.diff_subset, Set.Subset.trans, Set.inter_subset_left
-- 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
⊢ vᶜ \ uᶜ ∩ t ⊆ vᶜ

Tactic:
exact Set.Subset.trans Set.inter_subset_left diff_subset

Premises used: Set.diff_subset, Set.Subset.trans, Set.inter_subset_left
-- 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
⊢ uᶜ ∩ t ⊆ uᶜ

Tactic:
Set.inter_subset_left

Premises used: Set.inter_subset_left
-- 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
⊢ uᶜ ∩ t ⊆ uᶜ

Tactic:
exact Set.inter_subset_left

Premises used: Set.inter_subset_left
-- 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
⊢ Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)

Tactic:
disjoint_sdiff_self_right.mono Set.inter_subset_left Set.inter_subset_left

Premises used: disjoint_sdiff_self_right, Set.inter_subset_left, Disjoint.mono
-- 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
⊢ Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)

Tactic:
exact disjoint_sdiff_self_right.mono Set.inter_subset_left Set.inter_subset_left

Premises used: disjoint_sdiff_self_right, Set.inter_subset_left, Disjoint.mono
-- 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
h₁ : t ⊆ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
h₂ : uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t ⊆ t
⊢ t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
apply Set.Subset.antisymm

Premises used: Set.Subset.antisymm