awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have mp₁ : (↑μ : Set α → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
Tactic: rw [← hs, ennrealToMeasure_apply hmeas]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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∞)
⊢ (↑v : Set α → M) s = 0
have pos : ∀ (hmeas : MeasurableSet s), (↑v : Set α → M) s = 0
Tactic: by_cases hmeas : MeasurableSet s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑v : Set α → M) s = 0
have neg : ∀ (hmeas : ¬MeasurableSet s), (↑v : Set α → M) s = 0
Tactic: by_cases hmeas : MeasurableSet s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
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
have hs₁ : (↑μ : Set α → ℝ≥0∞) s = 0
Tactic: rw [ennrealToMeasure_apply hmeas] at hs
Cleared hypotheses: hs, hmeas
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
have refine_1 : ∀ (t : Set α) (hst : t ⊆ s), (↑v : Set α → M) t = 0
Tactic: refine ⟨s, hs, fun t hst => ?_, fun t hst => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ v ⟂ᵥ w
have refine_2 : ∀ (t : Set α) (hst : t ⊆ sᶜ), (↑w : Set α → N) t = 0
Tactic: refine ⟨s, hs, fun t hst => ?_, fun t hst => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑v : Set α → M) t = 0
have pos : ∀ (ht : MeasurableSet t), (↑v : Set α → M) t = 0
Tactic: by_cases ht : MeasurableSet t
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑v : Set α → M) t = 0
have neg : ∀ (ht : ¬MeasurableSet t), (↑v : Set α → M) t = 0
Tactic: by_cases ht : MeasurableSet t
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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ᶜ
⊢ (↑w : Set α → N) t = 0
have pos : ∀ (ht : MeasurableSet t), (↑w : Set α → N) t = 0
Tactic: by_cases ht : MeasurableSet t
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑w : Set α → N) t = 0
have neg : ∀ (ht : ¬MeasurableSet t), (↑w : Set α → N) t = 0
Tactic: by_cases ht : MeasurableSet t
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ v₁ + v₂ ⟂ᵥ w
have 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
Tactic: obtain ⟨u, hmu, hu₁, hu₂⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ v₁ + v₂ ⟂ᵥ w
have 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
Tactic: obtain ⟨v, hmv, hv₁, hv₂⟩ := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
have refine_1 : ∀ (t : Set α) (ht : t ⊆ u ∩ v), MeasurableSet t → (↑(v₁ + v₂) : Set α → M) t = 0
Tactic: refine mk (u ∩ v) (hmu.inter hmv) (fun t ht _ => ?_) fun t ht hmt => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ v₁ + v₂ ⟂ᵥ w
have refine_2 : ∀ (t : Set α) (ht : t ⊆ (u ∩ v)ᶜ) (hmt : MeasurableSet t), (↑w : Set α → N) t = 0
Tactic: refine mk (u ∩ v) (hmu.inter hmv) (fun t ht _ => ?_) fun t ht hmt => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v₁ + v₂) : Set α → M) t = 0
have refine_1 : (↑v₁ : Set α → M) t + (↑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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v₁ + v₂) : Set α → M) t = 0
have refine_1₁ : 0 + (↑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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v₁ + v₂) : Set α → M) t = 0
have refine_1₂ : HAdd.hAdd (α := M) 0 0 = 0
Tactic: rw [add_apply, hu₁ _ (Set.subset_inter_iff.1 ht).1, hv₁ _ (Set.subset_inter_iff.1 ht).2,
      zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v₁ + v₂) : Set α → M) t = 0
have refine_1₃ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [add_apply, hu₁ _ (Set.subset_inter_iff.1 ht).1, hv₁ _ (Set.subset_inter_iff.1 ht).2,
      zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
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
⊢ (↑w : Set α → N) t = 0
have ht₁ : t ⊆ uᶜ ∪ vᶜ
Tactic: rw [Set.compl_inter] at ht
Cleared hypotheses: ht, hmt
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑w : Set α → N) t = 0
have refine_2 : vᶜ \ uᶜ ∩ t ⊆ vᶜ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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ᶜ
⊢ (↑w : Set α → N) t = 0
have refine_2₁ : uᶜ ∩ t ⊆ uᶜ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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ᶜ
⊢ (↑w : Set α → N) t = 0
have rw : Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ (↑w : Set α → N) t = 0
have rw₁ : t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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ᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
have h₁ : t ⊆ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
have h₂ : uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t ⊆ t
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
have pos : ∀ (hxu' : x ∈ uᶜ), x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
Tactic: by_cases hxu' : x ∈ uᶜ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
have neg : ∀ (hxu' : x ∉ uᶜ), x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
Tactic: by_cases hxu' : x ∈ uᶜ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
have neg : ∀ (hxu : x ∈ uᶜ), x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
Tactic: rcases ht hx with (hxu | hxv)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
have neg₁ : ∀ (hxv : x ∈ vᶜ), x ∈ uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
Tactic: rcases ht hx with (hxu | hxv)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ x ∈ t
have h₂ : ∀ (hx : x ∈ uᶜ ∩ t), x ∈ t
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ x ∈ t
have h₃ : ∀ (hx : x ∈ vᶜ \ uᶜ ∩ t), x ∈ t
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ -v ⟂ᵥ w
have obtain : ∀ (u : Set α) (hmu : MeasurableSet u) (hu₁ : ∀ t ⊆ u, (↑v : Set α → M) t = 0) (hu₂ : ∀ t ⊆ uᶜ, (↑w : Set α → N) t = 0),
  -v ⟂ᵥ w
Tactic: obtain ⟨u, hmu, hu₁, hu₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
have refine : ∀ (s : Set α) (hs : s ⊆ u), (↑(-v) : Set α → M) s = 0
Tactic: refine ⟨u, hmu, fun s hs => ?_, hu₂⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
have rw : (↑v : Set α → M) s = 0
Tactic: rw [neg_apply v s, neg_eq_zero]