awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) ((↑v : Set α → M) i) : N) (0 : N)
have rw : Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
Tactic: rw [not_measurable v hi, AddMonoidHom.map_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) ((↑v : Set α → M) i) : N) (0 : N)
have rw₁ : Eq.{u_4 + 1} (α := N) 0 0
Tactic: rw [not_measurable v hi, AddMonoidHom.map_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
⊢ v.mapRange (AddMonoidHom.id M) ⋯ = v
have h : ∀ (i : Set α), MeasurableSet i → (↑(v.mapRange (AddMonoidHom.id M) sorry) : Set α → M) i = (↑v : Set α → M) i
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ Eq (α := VectorMeasure α N) (mapRange 0 f hf) 0
have h : ∀ (i : Set α), MeasurableSet i → (↑(mapRange 0 f hf) : Set α → N) i = (↑0 : Set α → N) i
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf
have h : ∀ (i : Set α),
  MeasurableSet i → (↑((v + w).mapRange f hf) : Set α → N) i = (↑(v.mapRange f hf + w.mapRange f hf) : Set α → N) i
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (m_1 • x).mapRange f.toAddMonoidHom hf =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m_1 : R) (x.mapRange f.toAddMonoidHom hf)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 : ℕ) ↦ 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)
have h : ∀ (x : ℕ), (if MeasurableSet (f x) then (↑v : Set α → M) (f x ∩ i) else 0) = (↑v : Set α → M) (f x ∩ i)
Tactic: convert!
          v.m_iUnion (fun n => (hf₁ n).inter hi)
            (hf₂.mono fun i j => Disjoint.mono inf_le_left inf_le_left)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: convert!
          v.m_iUnion (fun n => (hf₁ n).inter hi)
            (hf₂.mono fun i j => Disjoint.mono inf_le_left inf_le_left)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 : ℕ
⊢ (if MeasurableSet (f x) then (↑v : Set α → M) (f x ∩ i) else 0) = (↑v : Set α → M) (f x ∩ i)
have h : (↑v : Set α → M) (f x ∩ i) = (↑v : Set α → M) (f x ∩ i)
Tactic: rw [if_pos (hf₁ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: rw [Set.iUnion_inter, if_pos (MeasurableSet.iUnion hf₁)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ (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)
have h₁ : (↑v : Set α → M) (⋃ (i_1 : ℕ), f i_1 ∩ i) = (↑v : Set α → M) (⋃ (i_1 : ℕ), f i_1 ∩ i)
Tactic: rw [Set.iUnion_inter, if_pos (MeasurableSet.iUnion hf₁)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v.restrict i) : Set α → M) j = (↑v : Set α → M) (j ∩ i)
have rw : (↑{ measureOf' := fun (s : Set α) ↦ if MeasurableSet s then (↑v : Set α → M) (s ∩ i) else 0, empty' := sorry,
          not_measurable' := sorry, m_iUnion' := sorry : VectorMeasure α M } :
      Set α → M)
    j =
  (↑v : Set α → M) (j ∩ i)
Tactic: rw [restrict, dif_pos hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v.restrict i) : Set α → M) j = (↑v : Set α → M) j
have rw : (↑v : Set α → M) (j ∩ i) = (↑v : Set α → M) j
Tactic: rw [restrict_apply v hi hj, Set.inter_eq_left.2 hij]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v.restrict i) : Set α → M) j = (↑v : Set α → M) j
have rw₁ : (↑v : Set α → M) j = (↑v : Set α → M) j
Tactic: rw [restrict_apply v hi hj, Set.inter_eq_left.2 hij]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 ∅) : Set α → M) i = (↑0 : Set α → M) i
have rw : (↑v : Set α → M) (i ∩ ∅) = (↑0 : Set α → M) i
Tactic: rw [restrict_apply v MeasurableSet.empty hi, Set.inter_empty, v.empty, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v.restrict ∅) : Set α → M) i = (↑0 : Set α → M) i
have rw₁ : (↑v : Set α → M) ∅ = (↑0 : Set α → M) i
Tactic: rw [restrict_apply v MeasurableSet.empty hi, Set.inter_empty, v.empty, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v.restrict ∅) : Set α → M) i = (↑0 : Set α → M) i
have rw₂ : Eq.{u_3 + 1} (α := M) 0 ((↑0 : Set α → M) i)
Tactic: rw [restrict_apply v MeasurableSet.empty hi, Set.inter_empty, v.empty, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ (↑(v.restrict ∅) : Set α → M) i = (↑0 : Set α → M) i
have rw₃ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [restrict_apply v MeasurableSet.empty hi, Set.inter_empty, v.empty, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 univ) : Set α → M) i = (↑v : Set α → M) i
have rw : (↑v : Set α → M) (i ∩ univ) = (↑v : Set α → M) i
Tactic: rw [restrict_apply v MeasurableSet.univ hi, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ (↑(v.restrict univ) : Set α → M) i = (↑v : Set α → M) i
have rw₁ : (↑v : Set α → M) i = (↑v : Set α → M) i
Tactic: rw [restrict_apply v MeasurableSet.univ hi, Set.inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
i : Set α
⊢ Eq (α := VectorMeasure α M) (restrict 0 i) 0
have pos : ∀ (hi : MeasurableSet i), Eq (α := VectorMeasure α M) (restrict 0 i) 0
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ Eq (α := VectorMeasure α M) (restrict 0 i) 0
have neg : ∀ (hi : ¬MeasurableSet i), Eq (α := VectorMeasure α M) (restrict 0 i) 0
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
have pos : ∀ (j : Set α) (hj : MeasurableSet j), Eq.{u_3 + 1} (α := M) ((↑(restrict 0 i) : Set α → M) j) ((↑0 : Set α → M) j)
Tactic: ext j hj
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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
⊢ Eq.{u_3 + 1} (α := M) ((↑(restrict 0 i) : Set α → M) j) ((↑0 : Set α → M) j)
have pos : Eq.{u_3 + 1} (α := M) ((↑0 : Set α → M) (j ∩ i)) ((↑0 : Set α → M) j)
Tactic: rw [restrict_apply 0 hi hj, zero_apply, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((↑(restrict 0 i) : Set α → M) j) ((↑0 : Set α → M) j)
have pos₁ : Eq.{u_3 + 1} (α := M) 0 ((↑0 : Set α → M) j)
Tactic: rw [restrict_apply 0 hi hj, zero_apply, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ Eq.{u_3 + 1} (α := M) ((↑(restrict 0 i) : Set α → M) j) ((↑0 : Set α → M) j)
have pos₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [restrict_apply 0 hi hj, zero_apply, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 : α → β
⊢ (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)
have pos : ∀ (hf : Measurable f), (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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)
⊢ (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)
have neg : ∀ (hf : ¬Measurable f), (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
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 : α → β
hf : Measurable f
⊢ (v + w).map f = HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)
have pos : ∀ (i : Set β) (hi : MeasurableSet i),
  (↑((v + w).map f) : Set β → M) i = (↑(HAdd.hAdd (α := VectorMeasure β M) (v.map f) (w.map f)) : Set β → M) i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
⊢ (v + w).restrict i = v.restrict i + w.restrict i
have pos : ∀ (hi : MeasurableSet i), (v + w).restrict i = v.restrict i + w.restrict i
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
pos : ∀ (hi : MeasurableSet i), (v + w).restrict i = v.restrict i + w.restrict i
⊢ (v + w).restrict i = v.restrict i + w.restrict i
have neg : ∀ (hi : ¬MeasurableSet i), (v + w).restrict i = v.restrict i + w.restrict i
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (v + w).restrict i = v.restrict i + w.restrict i
have pos : ∀ (j : Set α) (hj : MeasurableSet j),
  (↑((v + w).restrict i) : Set α → M) j = (↑(v.restrict i + w.restrict i) : Set α → M) j
Tactic: ext j hj
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : T2Space M
inst_4 : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ v.restrict i + v.restrict iᶜ = v
have h : ∀ (A : Set α) (hA : MeasurableSet A), (↑(v.restrict i + v.restrict iᶜ) : Set α → M) A = (↑v : Set α → M) A
Tactic: ext A hA
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : T2Space M
inst_4 : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
⊢ (↑(v.restrict i + v.restrict iᶜ) : Set α → M) A = (↑v : Set α → M) A
have h : (↑v : Set α → M) (A ∩ i ∪ A ∩ iᶜ) = (↑v : Set α → M) A
Tactic: rw [add_apply, restrict_apply _ hi hA, restrict_apply _ hi.compl hA,
    ← of_union _ (hA.inter hi) (hA.inter hi.compl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : T2Space M
inst_4 : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
h : (↑v : Set α → M) (A ∩ i ∪ A ∩ iᶜ) = (↑v : Set α → M) A
⊢ (↑(v.restrict i + v.restrict iᶜ) : Set α → M) A = (↑v : Set α → M) A
have rw : Disjoint (A ∩ i) (A ∩ iᶜ)
Tactic: rw [add_apply, restrict_apply _ hi hA, restrict_apply _ hi.compl hA,
    ← of_union _ (hA.inter hi) (hA.inter hi.compl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
⊢ (-v).restrict i = -v.restrict i
have pos : ∀ (hi : MeasurableSet i), (-v).restrict i = -v.restrict i
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
pos : ∀ (hi : MeasurableSet i), (-v).restrict i = -v.restrict i
⊢ (-v).restrict i = -v.restrict i
have neg : ∀ (hi : ¬MeasurableSet i), (-v).restrict i = -v.restrict i
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (-v).restrict i = -v.restrict i
have pos : ∀ (j : Set α) (hj : MeasurableSet j), (↑((-v).restrict i) : Set α → M) j = (↑(-v.restrict i) : Set α → M) j
Tactic: ext j hj
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
⊢ (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)
have pos : ∀ (hf : Measurable f), (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
pos : ∀ (hf : Measurable f), (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)
⊢ (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)
have neg : ∀ (hf : ¬Measurable f), (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : Measurable f
⊢ (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)
have pos : ∀ (i : Set β) (hi : MeasurableSet i),
  (↑((c • v).map f) : Set β → M) i = (↑(HSMul.hSMul (β := VectorMeasure β M) c (v.map f)) : Set β → M) i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ (c • v).map f = HSMul.hSMul (β := VectorMeasure β M) c (v.map f)
have neg : 0 = HSMul.hSMul (β := VectorMeasure β M) c 0
Tactic: simp only [map, dif_neg hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
R : Type u_4
inst_3 : Semiring R
inst_4 : DistribMulAction R M
inst_5 : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ 0 = HSMul.hSMul (β := VectorMeasure β M) c 0
have neg : ∀ (i : Set β), MeasurableSet i → (↑0 : Set β → M) i = (↑(HSMul.hSMul (β := VectorMeasure β M) c 0) : Set β → M) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
v : VectorMeasure α M
i : Set α
c : R
⊢ (c • v).restrict i = c • v.restrict i
have pos : ∀ (hi : MeasurableSet i), (c • v).restrict i = c • v.restrict i
Tactic: by_cases hi : MeasurableSet i