awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ HasSum (fun (i : ℕ) ↦ (↑v : Set α → M) (f ⁻¹' g i)) ((↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i))

Tactic:
v.m_iUnion (fun i => hf (hg₁ i)) fun i j hij => (hg₂ hij).preimage _

Premises used: MeasureTheory.VectorMeasure.m_iUnion, Disjoint.preimage
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
h : ∀ (x : ℕ), (if MeasurableSet (g x) then (↑v : Set α → M) (f ⁻¹' g x) else 0) = (↑v : Set α → M) (f ⁻¹' g x)
h₁ :
  (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (f ⁻¹' ⋃ (i : ℕ), g i) else 0) =
    (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (g i) then (↑v : Set α → M) (f ⁻¹' g i) else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (f ⁻¹' ⋃ (i : ℕ), g i) else 0)

Tactic:
convert! v.m_iUnion (fun i => hf (hg₁ i)) fun i j hij => (hg₂ hij).preimage _

Premises used: MeasureTheory.VectorMeasure.m_iUnion, Disjoint.preimage
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
x : ℕ
h h₁ : (↑v : Set α → M) (f ⁻¹' g x) = (↑v : Set α → M) (f ⁻¹' g x)
⊢ (if MeasurableSet (g x) then (↑v : Set α → M) (f ⁻¹' g x) else 0) = (↑v : Set α → M) (f ⁻¹' g x)

Tactic:
rw [if_pos (hg₁ _)]

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
h :
  (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i) else 0) =
    (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)
h₁ h₂ : (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i) = (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)
⊢ (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (f ⁻¹' ⋃ (i : ℕ), g i) else 0) =
    (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)

Tactic:
rw [Set.preimage_iUnion, if_pos (MeasurableSet.iUnion hg₁)]

Premises used: if_pos, Set.preimage_iUnion, MeasurableSet.iUnion
-- 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
v : VectorMeasure α M
f : α → β
hf : ¬Measurable f
⊢ Eq (α := VectorMeasure β M) (v.map f) 0

Tactic:
dif_neg hf

Premises used: dif_neg, MeasureTheory.VectorMeasure.map
-- 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
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
rw :
  (↑{ measureOf' := fun (s : Set β) ↦ if MeasurableSet s then (↑v : Set α → M) (f ⁻¹' s) else 0, empty' := ⋯,
            not_measurable' := ⋯, m_iUnion' := ⋯ : VectorMeasure β M } :
        Set β → M)
      s =
    (↑v : Set α → M) (f ⁻¹' s)
⊢ (↑(v.map f) : Set β → M) s = (↑v : Set α → M) (f ⁻¹' s)

Tactic:
rw [map, dif_pos hf]

Premises used: dif_pos, MeasureTheory.VectorMeasure.map
-- 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
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (↑{ measureOf' := fun (s : Set β) ↦ if MeasurableSet s then (↑v : Set α → M) (f ⁻¹' s) else 0, empty' := ⋯,
            not_measurable' := ⋯, m_iUnion' := ⋯ : VectorMeasure β M } :
        Set β → M)
      s =
    (↑v : Set α → M) (f ⁻¹' s)

Tactic:
if_pos hs

Premises used: if_pos, ite
-- 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
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (↑{ measureOf' := fun (s : Set β) ↦ if MeasurableSet s then (↑v : Set α → M) (f ⁻¹' s) else 0, empty' := ⋯,
            not_measurable' := ⋯, m_iUnion' := ⋯ : VectorMeasure β M } :
        Set β → M)
      s =
    (↑v : Set α → M) (f ⁻¹' s)

Tactic:
exact if_pos hs

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
rw : (↑v : Set α → M) (id ⁻¹' i) = (↑v : Set α → M) i
rw₁ rw₂ : (↑v : Set α → M) i = (↑v : Set α → M) i
⊢ (↑(v.map id) : Set α → M) i = (↑v : Set α → M) i

Tactic:
rw [map_apply v measurable_id hi, Set.preimage_id]

Premises used: measurable_id, Set.preimage_id, 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
f : α → β
pos : ∀ (hf : Measurable f), Eq (α := VectorMeasure β M) (map 0 f) 0
neg : ∀ (hf : ¬Measurable f), Eq (α := VectorMeasure β M) (map 0 f) 0
⊢ Eq (α := VectorMeasure β M) (map 0 f) 0

Tactic:
by_cases hf : Measurable f

Premises used: Measurable
-- 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
f : α → β
hf : Measurable f
pos : ∀ (i : Set β) (hi : MeasurableSet i), Eq.{u_3 + 1} (α := M) ((↑(map 0 f) : Set β → M) i) ((↑0 : Set β → M) i)
⊢ Eq (α := VectorMeasure β M) (map 0 f) 0

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
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
pos : Eq.{u_3 + 1} (α := M) ((↑0 : Set α → M) (f ⁻¹' i)) ((↑0 : Set β → M) i)
pos₁ : Eq.{u_3 + 1} (α := M) 0 ((↑0 : Set β → M) i)
pos₂ pos₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ Eq.{u_3 + 1} (α := M) ((↑(map 0 f) : Set β → M) i) ((↑0 : Set β → M) i)

Tactic:
rw [map_apply _ hf hi, zero_apply, zero_apply]

Premises used: MeasureTheory.VectorMeasure.zero_apply, 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
f : α → β
hf : ¬Measurable f
⊢ Eq (α := VectorMeasure β M) (map 0 f) 0

Tactic:
dif_neg hf

Premises used: dif_neg, MeasureTheory.VectorMeasure.map
-- 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
f : α → β
hf : ¬Measurable f
⊢ Eq (α := VectorMeasure β M) (map 0 f) 0

Tactic:
exact dif_neg hf

Premises used: dif_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 : VectorMeasure α M
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
v : VectorMeasure α M
f : M →+ N
hf : Continuous[inst_3, inst_5] (⇑f : (a : M) → N)
rw : Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
rw₁ rw₂ : Eq.{u_4 + 1} (α := N) 0 0
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) ((↑v : Set α → M) ∅) : N) (0 : N)

Tactic:
rw [empty, AddMonoidHom.map_zero]

Premises used: MeasureTheory.VectorMeasure.empty, AddMonoidHom.map_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 : VectorMeasure α M
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
v : VectorMeasure α M
f : M →+ N
hf : Continuous[inst_3, inst_5] (⇑f : (a : M) → N)
i : Set α
hi : ¬MeasurableSet i
rw : Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
rw₁ rw₂ : Eq.{u_4 + 1} (α := N) 0 0
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) ((↑v : Set α → M) i) : N) (0 : N)

Tactic:
rw [not_measurable v hi, AddMonoidHom.map_zero]

Premises used: AddMonoidHom.map_zero, MeasureTheory.VectorMeasure.not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : TopologicalSpace N
f : M →+ N
hf : Continuous[inst_2, inst_4] (⇑f : (a : M) → N)
s : Set α
⊢ (↑(v.mapRange f hf) : Set α → N) s = (f : (a : M) → N) ((↑v : Set α → M) s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → (↑(v.mapRange (AddMonoidHom.id M) ⋯) : Set α → M) i = (↑v : Set α → M) i
⊢ v.mapRange (AddMonoidHom.id M) ⋯ = v

Tactic:
ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
h : MeasurableSet i
⊢ (↑(v.mapRange (AddMonoidHom.id M) ⋯) : Set α → M) i = (↑v : Set α → M) i

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : TopologicalSpace N
f : M →+ N
hf : Continuous[inst_2, inst_4] (⇑f : (a : M) → N)
h : ∀ (i : Set α), MeasurableSet i → (↑(mapRange 0 f hf) : Set α → N) i = (↑0 : Set α → N) i
⊢ Eq (α := VectorMeasure α N) (mapRange 0 f hf) 0

Tactic:
ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : TopologicalSpace N
f : M →+ N
hf : Continuous[inst_2, inst_4] (⇑f : (a : M) → N)
i : Set α
h : MeasurableSet i
⊢ (↑(mapRange 0 f hf) : Set α → N) i = (↑0 : Set α → N) i

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : TopologicalSpace N
inst_5 : ContinuousAdd M
inst_6 : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous[inst_2, inst_4] (⇑f : (a : M) → N)
h :
  ∀ (i : Set α),
    MeasurableSet i → (↑((v + w).mapRange f hf) : Set α → N) i = (↑(v.mapRange f hf + w.mapRange f hf) : Set α → N) i
⊢ (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf

Tactic:
ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
N : Type u_4
inst_3 : AddCommMonoid N
inst_4 : TopologicalSpace N
inst_5 : ContinuousAdd M
inst_6 : ContinuousAdd N
v w : VectorMeasure α M
f : M →+ N
hf : Continuous[inst_2, inst_4] (⇑f : (a : M) → N)
i : Set α
h : MeasurableSet i
⊢ (↑((v + w).mapRange f hf) : Set α → N) i = (↑(v.mapRange f hf + w.mapRange f hf) : Set α → N) i

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v : VectorMeasure α M
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
R : Type u_5
inst_6 : Semiring R
inst_7 : Module R M
inst_8 : Module R N
inst_9 : ContinuousAdd M
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R M
inst_12 : ContinuousConstSMul R N
f : M →ₗ[R] N
hf : Continuous[inst_3, inst_5] (⇑f : (a : M) → N)
m_1 : R
x : VectorMeasure α M
h :
  ∀ (i : Set α),
    MeasurableSet i →
      (↑((m_1 • x).mapRange f.toAddMonoidHom hf) : Set α → N) i =
        (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m_1 : R) (x.mapRange f.toAddMonoidHom hf)) : Set α → N) i
⊢ (m_1 • x).mapRange f.toAddMonoidHom hf =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m_1 : R) (x.mapRange f.toAddMonoidHom hf)

Tactic:
ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v : VectorMeasure α M
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
R : Type u_5
inst_6 : Semiring R
inst_7 : Module R M
inst_8 : Module R N
inst_9 : ContinuousAdd M
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R M
inst_12 : ContinuousConstSMul R N
f : M →ₗ[R] N
hf : Continuous[inst_3, inst_5] (⇑f : (a : M) → N)
m_1 : R
x : VectorMeasure α M
i : Set α
h : MeasurableSet i
⊢ (↑((m_1 • x).mapRange f.toAddMonoidHom hf) : Set α → N) i =
    (↑(HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m_1 : R) (x.mapRange f.toAddMonoidHom hf)) : Set α → N) i

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (if MeasurableSet.{u_1} (α := α) ∅ then (↑v : Set α → M) (∅ ∩ i) else 0) = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun (i_1 : ℕ) ↦ (↑v : Set α → M) (f i_1 ∩ i)) ((↑v : Set α → M) (⋃ (i_1 : ℕ), f i_1 ∩ i))

Tactic:
v.m_iUnion (fun n => (hf₁ n).inter hi)
            (hf₂.mono fun i j => Disjoint.mono inf_le_left inf_le_left)

Premises used: Disjoint.mono, inf_le_left, MeasureTheory.VectorMeasure.m_iUnion, Pairwise.mono, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h : ∀ (x : ℕ), (if MeasurableSet (f x) then (↑v : Set α → M) (f x ∩ i) else 0) = (↑v : Set α → M) (f x ∩ i)
h₁ :
  (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) ((⋃ (i : ℕ), f i) ∩ i) else 0) =
    (↑v : Set α → M) (⋃ (i_1 : ℕ), f i_1 ∩ i)
⊢ HasSum (fun (i_1 : ℕ) ↦ if MeasurableSet (f i_1) then (↑v : Set α → M) (f i_1 ∩ i) else 0)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) ((⋃ (i : ℕ), f i) ∩ i) else 0)

Tactic:
convert!
          v.m_iUnion (fun n => (hf₁ n).inter hi)
            (hf₂.mono fun i j => Disjoint.mono inf_le_left inf_le_left)

Premises used: Disjoint.mono, inf_le_left, MeasureTheory.VectorMeasure.m_iUnion, Pairwise.mono, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
x : ℕ
h h₁ : (↑v : Set α → M) (f x ∩ i) = (↑v : Set α → M) (f x ∩ i)
⊢ (if MeasurableSet (f x) then (↑v : Set α → M) (f x ∩ i) else 0) = (↑v : Set α → M) (f x ∩ i)

Tactic:
rw [if_pos (hf₁ _)]

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h :
  (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) (⋃ (i_1 : ℕ), f i_1 ∩ i) else 0) =
    (↑v : Set α → M) (⋃ (i_1 : ℕ), f i_1 ∩ i)
h₁ h₂ : (↑v : Set α → M) (⋃ (i_1 : ℕ), f i_1 ∩ i) = (↑v : Set α → M) (⋃ (i_1 : ℕ), f i_1 ∩ i)
⊢ (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) ((⋃ (i : ℕ), f i) ∩ i) else 0) =
    (↑v : Set α → M) (⋃ (i_1 : ℕ), f i_1 ∩ i)

Tactic:
rw [Set.iUnion_inter, if_pos (MeasurableSet.iUnion hf₁)]

Premises used: if_pos, Set.iUnion_inter, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ v.restrict i = 0

Tactic:
dif_neg hi

Premises used: dif_neg, MeasureTheory.VectorMeasure.restrict
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
rw :
  (↑{ measureOf' := fun (s : Set α) ↦ if MeasurableSet s then (↑v : Set α → M) (s ∩ i) else 0, empty' := ⋯,
            not_measurable' := ⋯, m_iUnion' := ⋯ : VectorMeasure α M } :
        Set α → M)
      j =
    (↑v : Set α → M) (j ∩ i)
⊢ (↑(v.restrict i) : Set α → M) j = (↑v : Set α → M) (j ∩ i)

Tactic:
rw [restrict, dif_pos hi]

Premises used: dif_pos, MeasureTheory.VectorMeasure.restrict
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (↑{ measureOf' := fun (s : Set α) ↦ if MeasurableSet s then (↑v : Set α → M) (s ∩ i) else 0, empty' := ⋯,
            not_measurable' := ⋯, m_iUnion' := ⋯ : VectorMeasure α M } :
        Set α → M)
      j =
    (↑v : Set α → M) (j ∩ i)

Tactic:
if_pos hj

Premises used: if_pos, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (↑{ measureOf' := fun (s : Set α) ↦ if MeasurableSet s then (↑v : Set α → M) (s ∩ i) else 0, empty' := ⋯,
            not_measurable' := ⋯, m_iUnion' := ⋯ : VectorMeasure α M } :
        Set α → M)
      j =
    (↑v : Set α → M) (j ∩ i)

Tactic:
exact if_pos hj

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
hij : j ⊆ i
rw : (↑v : Set α → M) (j ∩ i) = (↑v : Set α → M) j
rw₁ rw₂ : (↑v : Set α → M) j = (↑v : Set α → M) j
⊢ (↑(v.restrict i) : Set α → M) j = (↑v : Set α → M) j

Tactic:
rw [restrict_apply v hi hj, Set.inter_eq_left.2 hij]

Premises used: Set.inter_eq_left, Iff.mpr, 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
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
rw : (↑v : Set α → M) (i ∩ ∅) = (↑0 : Set α → M) i
rw₁ : (↑v : Set α → M) ∅ = (↑0 : Set α → M) i
rw₂ : Eq.{u_3 + 1} (α := M) 0 ((↑0 : Set α → M) i)
rw₃ rw₄ : Eq.{u_3 + 1} (α := M) 0 0
⊢ (↑(v.restrict ∅) : Set α → M) i = (↑0 : Set α → M) i

Tactic:
rw [restrict_apply v MeasurableSet.empty hi, Set.inter_empty, v.empty, zero_apply]

Premises used: MeasureTheory.VectorMeasure.empty, MeasurableSet.empty, MeasureTheory.VectorMeasure.zero_apply, MeasureTheory.VectorMeasure.restrict_apply, Set.inter_empty
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
rw : (↑v : Set α → M) (i ∩ univ) = (↑v : Set α → M) i
rw₁ rw₂ : (↑v : Set α → M) i = (↑v : Set α → M) i
⊢ (↑(v.restrict univ) : Set α → M) i = (↑v : Set α → M) i

Tactic:
rw [restrict_apply v MeasurableSet.univ hi, Set.inter_univ]

Premises used: Set.inter_univ, MeasureTheory.VectorMeasure.restrict_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
i : Set α
pos : ∀ (hi : MeasurableSet i), Eq (α := VectorMeasure α M) (restrict 0 i) 0
neg : ∀ (hi : ¬MeasurableSet i), Eq (α := VectorMeasure α M) (restrict 0 i) 0
⊢ Eq (α := VectorMeasure α M) (restrict 0 i) 0

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
i : Set α
hi : MeasurableSet i
pos : ∀ (j : Set α) (hj : MeasurableSet j), Eq.{u_3 + 1} (α := M) ((↑(restrict 0 i) : Set α → M) j) ((↑0 : Set α → M) j)
⊢ Eq (α := VectorMeasure α M) (restrict 0 i) 0

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
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
pos : Eq.{u_3 + 1} (α := M) ((↑0 : Set α → M) (j ∩ i)) ((↑0 : Set α → M) j)
pos₁ : Eq.{u_3 + 1} (α := M) 0 ((↑0 : Set α → M) j)
pos₂ pos₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ Eq.{u_3 + 1} (α := M) ((↑(restrict 0 i) : Set α → M) j) ((↑0 : Set α → M) j)

Tactic:
rw [restrict_apply 0 hi hj, zero_apply, zero_apply]

Premises used: MeasureTheory.VectorMeasure.zero_apply, MeasureTheory.VectorMeasure.restrict_apply, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
i : Set α
hi : ¬MeasurableSet i
⊢ Eq (α := VectorMeasure α M) (restrict 0 i) 0

Tactic:
dif_neg hi

Premises used: dif_neg, MeasureTheory.VectorMeasure.restrict
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
i : Set α
hi : ¬MeasurableSet i
⊢ Eq (α := VectorMeasure α M) (restrict 0 i) 0

Tactic:
exact dif_neg hi

Premises used: dif_neg
-- 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 : α → β
pos : ∀ (hf : Measurable f), (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)
neg : ∀ (hf : ¬Measurable f), (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)
⊢ (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)

Tactic:
by_cases hf : Measurable f

Premises used: Measurable