-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem add_left [T2Space N] [ContinuousAdd M] (h₁ : v₁ ⟂ᵥ w) (h₂ : v₂ ⟂ᵥ w) : v₁ + v₂ ⟂ᵥ w

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w 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:
rcases ht hx with (hxu | hxv)

Result:
case neg.inl
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w 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

case neg.inr
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w 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

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w

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

Result:
case intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
t : Set α
ht : t ⊆ u ∩ v
x✝ : MeasurableSet t
⊢ ↑(v₁ + v₂) t = 0

case intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
t : Set α
ht : t ⊆ (u ∩ v)ᶜ
hmt : MeasurableSet t
⊢ ↑w t = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w 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

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
h₂ : v₂ ⟂ᵥ w
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w

Tactic:
obtain ⟨v, hmv, hv₁, hv₂⟩ := h₂

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
⊢ v₁ + v₂ ⟂ᵥ w

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ ↑w 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]

Result:
case intro.intro.intro.intro.intro.intro.refine_2.a
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ vᶜ \ uᶜ ∩ t ⊆ vᶜ

case intro.intro.intro.intro.intro.intro.refine_2.a
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ uᶜ ∩ t ⊆ uᶜ

α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)

α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, ↑v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, ↑w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, ↑v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, ↑w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t