awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[bif false then i else j] w

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedAddMonoid M
inst_4 : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[bif true then i else j] w

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
pos : ∀ (hi₁ : MeasurableSet i), 0 ≤ (↑v : Set α → M) i
neg : ∀ (hi₁ : ¬MeasurableSet i), 0 ≤ (↑v : Set α → M) i
⊢ 0 ≤ (↑v : Set α → M) i

Tactic:
by_cases hi₁ : MeasurableSet i

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
hi₁ : MeasurableSet i
⊢ 0 ≤ (↑v : Set α → M) i

Tactic:
(restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl

Premises used: Set.Subset.rfl, Iff.mp, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
hi₁ : MeasurableSet i
⊢ 0 ≤ (↑v : Set α → M) i

Tactic:
exact (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl

Premises used: Set.Subset.rfl, Iff.mp, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
hi₁ : ¬MeasurableSet i
neg neg₁ : LE.le.{u_3} (α := M) 0 0
⊢ 0 ≤ (↑v : Set α → M) i

Tactic:
rw [v.not_measurable hi₁]

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
pos : ∀ (hi₁ : MeasurableSet i), (↑v : Set α → M) i ≤ 0
neg : ∀ (hi₁ : ¬MeasurableSet i), (↑v : Set α → M) i ≤ 0
⊢ (↑v : Set α → M) i ≤ 0

Tactic:
by_cases hi₁ : MeasurableSet i

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
hi₁ : MeasurableSet i
⊢ (↑v : Set α → M) i ≤ 0

Tactic:
(restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl

Premises used: Set.Subset.rfl, Iff.mp, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
hi₁ : MeasurableSet i
⊢ (↑v : Set α → M) i ≤ 0

Tactic:
exact (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl

Premises used: Set.Subset.rfl, Iff.mp, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi₂ : v ≤[i] 0
hi₁ : ¬MeasurableSet i
neg neg₁ : LE.le.{u_3} (α := M) 0 0
⊢ (↑v : Set α → M) i ≤ 0

Tactic:
rw [v.not_measurable hi₁]

Premises used: MeasureTheory.VectorMeasure.not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
rw : 0 ≤ v.restrict i
rw₁ rw₂ : LE.le (α := VectorMeasure α M) 0 0
⊢ 0 ≤[i] v

Tactic:
rw [restrict_zero, restrict_not_measurable _ hi]

Premises used: MeasureTheory.VectorMeasure.restrict_not_measurable, MeasureTheory.VectorMeasure.restrict_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
rw : v.restrict i ≤ 0
rw₁ rw₂ : LE.le (α := VectorMeasure α M) 0 0
⊢ v ≤[i] 0

Tactic:
rw [restrict_zero, restrict_not_measurable _ hi]

Premises used: MeasureTheory.VectorMeasure.restrict_not_measurable, MeasureTheory.VectorMeasure.restrict_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬0 ≤[i] v
⊢ MeasurableSet i

Tactic:
Not.imp_symm (zero_le_restrict_not_measurable _) hi

Premises used: Not.imp_symm, MeasureTheory.VectorMeasure.zero_le_restrict_not_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬v ≤[i] 0
⊢ MeasurableSet i

Tactic:
Not.imp_symm (restrict_le_zero_of_not_measurable _) hi

Premises used: MeasureTheory.VectorMeasure.restrict_le_zero_of_not_measurable, Not.imp_symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hij : j ⊆ i
hi₂ : 0 ≤[i] v
⊢ 0 ≤[j] v

Tactic:
restrict_le_restrict_of_subset_le _ _ fun _ hk₁ hk₂ =>
    (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hk₁ (Set.Subset.trans hk₂ hij)

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le, Set.Subset.trans, Iff.mp, OfNat.ofNat, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
v : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hij : j ⊆ i
hi₂ : v ≤[i] 0
⊢ v ≤[j] 0

Tactic:
restrict_le_restrict_of_subset_le _ _ fun _ hk₁ hk₂ =>
    (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hk₁ (Set.Subset.trans hk₂ hij)

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le, Set.Subset.trans, Iff.mp, OfNat.ofNat, MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
v : VectorMeasure α M
i : Set α
hi : ¬v ≤[i] 0
⊢ MeasurableSet i

Tactic:
have hi₁ : MeasurableSet i := measurable_of_not_restrict_le_zero _ hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
v : VectorMeasure α M
i : Set α
hi : ¬v ≤[i] 0
hi₁ : MeasurableSet i
⊢ ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑0 : Set α → M) j

Tactic:
rw [restrict_le_restrict_iff _ _ hi₁] at hi

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
v : VectorMeasure α M
i : Set α
hi : ¬v ≤[i] 0
hi₁ : MeasurableSet i
hi₂ : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑0 : Set α → M) j
⊢ MeasurableSet i

Tactic:
rw [restrict_le_restrict_iff _ _ hi₁] at hi

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
v : VectorMeasure α M
i : Set α
hi : ¬∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑v : Set α → M) j ≤ (↑0 : Set α → M) j
hi₁ : MeasurableSet i
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ (↑0 : Set α → M) j < (↑v : Set α → M) j

Tactic:
push Not at hi

Premises used: Not
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
v : VectorMeasure α M
i : Set α
hi₁ : MeasurableSet i
hi : ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ (↑0 : Set α → M) j < (↑v : Set α → M) j
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ 0 < (↑v : Set α → M) j

Tactic:
hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : LinearOrder M
v : VectorMeasure α M
i : Set α
hi₁ : MeasurableSet i
hi : ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ (↑0 : Set α → M) j < (↑v : Set α → M) j
⊢ ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ 0 < (↑v : Set α → M) j

Tactic:
exact hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : AddLeftMono M
inst_4 : ContinuousAdd M
x x_1 x_2 : VectorMeasure α M
h : x_1 ≤ x_2
i : Set α
hi : MeasurableSet i
dsimp : (↑x : Set α → M) i + (↑x_1 : Set α → M) i ≤ (↑x : Set α → M) i + (↑x_2 : Set α → M) i
⊢ (↑(x + x_1) : Set α → M) i ≤ (↑(x + x_2) : Set α → M) i

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : PartialOrder M
inst_3 : AddLeftMono M
inst_4 : ContinuousAdd M
x x_1 x_2 : VectorMeasure α M
h : x_1 ≤ x_2
i : Set α
hi : MeasurableSet i
grw grw₁ : (↑x : Set α → M) i + (↑x_2 : Set α → M) i ≤ (↑x : Set α → M) i + (↑x_2 : Set α → M) i
⊢ (↑x : Set α → M) i + (↑x_1 : Set α → M) i ≤ (↑x : Set α → M) i + (↑x_2 : Set α → M) i

Tactic:
grw [h i hi]
-- 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 : ∀ ⦃s : Set α⦄, MeasurableSet s → (↑w : Set α → N) s = 0 → (↑v : Set α → M) s = 0
s : Set α
hs : (↑w : Set α → N) s = 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
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 : ∀ ⦃s : Set α⦄, MeasurableSet s → (↑w : Set α → N) s = 0 → (↑v : Set α → M) s = 0
s : Set α
hs : (↑w : Set α → N) s = 0
hmeas : MeasurableSet s
⊢ (↑v : Set α → M) s = 0

Tactic:
h hmeas hs
-- 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 : ∀ ⦃s : Set α⦄, MeasurableSet s → (↑w : Set α → N) s = 0 → (↑v : Set α → M) s = 0
s : Set α
hs : (↑w : Set α → N) s = 0
hmeas : MeasurableSet s
⊢ (↑v : Set α → M) s = 0

Tactic:
exact h hmeas hs
-- 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 : ∀ ⦃s : Set α⦄, MeasurableSet s → (↑w : Set α → N) s = 0 → (↑v : Set α → M) s = 0
s : Set α
hs : (↑w : Set α → N) s = 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
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 : ∀ ⦃s : Set α⦄, MeasurableSet s → (↑w : Set α → N) s = 0 → (↑v : Set α → M) s = 0
s : Set α
hs : (↑w : Set α → N) s = 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
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v w : VectorMeasure α M
h : v = w
⊢ v ≪ᵥ w

Tactic:
fun _ hs => h.symm ▸ hs

Premises used: Eq.rec, MeasureTheory.VectorMeasure.AbsolutelyContinuous, Eq.symm
-- 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
⊢ v ≪ᵥ v

Tactic:
eq rfl

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.eq, rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
u : VectorMeasure α L
v : VectorMeasure α M
w : VectorMeasure α N
huv : u ≪ᵥ v
hvw : v ≪ᵥ w
⊢ u ≪ᵥ w

Tactic:
fun _ hs => huv <| hvw hs

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous
-- 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 α N
⊢ AbsolutelyContinuous.{u_1, u_4, u_5} (M := M) 0 v

Tactic:
fun s _ => VectorMeasure.zero_apply s

Premises used: MeasureTheory.VectorMeasure.zero_apply, MeasureTheory.VectorMeasure.AbsolutelyContinuous
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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
s : Set α
hs : (↑w : Set α → N) s = 0
rw : -(↑v : Set α → M) s = 0
rw₁ : Eq.{u_6 + 1} (α := M) (-0) 0
rw₂ rw₃ : Eq.{u_6 + 1} (α := M) 0 0
⊢ (↑(-v) : Set α → M) s = 0

Tactic:
rw [neg_apply, h hs, neg_zero]

Premises used: MeasureTheory.VectorMeasure.neg_apply, neg_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
N : Type u_6
inst_2 : AddCommGroup N
inst_3 : TopologicalSpace N
inst_4 : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑(-w) : Set α → N) s = 0
⊢ (↑w : Set α → N) s = 0

Tactic:
rw [neg_apply, neg_eq_zero] at hs

Premises used: MeasureTheory.VectorMeasure.neg_apply, neg_eq_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
N : Type u_6
inst_2 : AddCommGroup N
inst_3 : TopologicalSpace N
inst_4 : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
⊢ (↑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
N : Type u_6
inst_2 : AddCommGroup N
inst_3 : TopologicalSpace N
inst_4 : IsTopologicalAddGroup N
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
⊢ (↑v : Set α → M) s = 0

Tactic:
exact h hs
-- 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
inst_4 : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : (↑v₁ : Set α → M) s + (↑v₂ : Set α → M) s = 0
rw₁ : 0 + (↑v₂ : Set α → M) s = 0
rw₂ : HAdd.hAdd (α := M) 0 0 = 0
rw₃ rw₄ : Eq.{u_4 + 1} (α := M) 0 0
⊢ (↑(v₁ + v₂) : Set α → M) s = 0

Tactic:
rw [add_apply, hv₁ hs, hv₂ hs, zero_add]

Premises used: zero_add, MeasureTheory.VectorMeasure.add_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : (↑v₁ : Set α → M) s - (↑v₂ : Set α → M) s = 0
rw₁ : 0 - (↑v₂ : Set α → M) s = 0
rw₂ : HSub.hSub (α := M) 0 0 = 0
rw₃ : Eq.{u_6 + 1} (α := M) (-0) 0
rw₄ rw₅ : Eq.{u_6 + 1} (α := M) 0 0
⊢ (↑(v₁ - v₂) : Set α → M) s = 0

Tactic:
rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]

Premises used: neg_zero, zero_sub, MeasureTheory.VectorMeasure.sub_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
R : Type u_6
inst_4 : Semiring R
inst_5 : DistribMulAction R M
inst_6 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
w : VectorMeasure α N
h : v ≪ᵥ w
s : Set α
hs : (↑w : Set α → N) s = 0
rw : r • (↑v : Set α → M) s = 0
rw₁ : HSMul.hSMul (β := M) r 0 = 0
rw₂ rw₃ : Eq.{u_4 + 1} (α := M) 0 0
⊢ (↑(r • v) : Set α → M) s = 0

Tactic:
rw [smul_apply, h hs, smul_zero]

Premises used: MeasureTheory.VectorMeasure.smul_apply, smul_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
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
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
pos : ∀ (hf : Measurable f), AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)
neg : ∀ (hf : ¬Measurable f), AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)
⊢ AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)

Tactic:
by_cases hf : Measurable f

Premises used: Measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
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
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
⊢ AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)

Tactic:
mk fun s hs hws => ?_

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
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
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
pos : ∀ (s : Set β) (hs : MeasurableSet s) (hws : (↑(w.map f) : Set β → N) s = 0), (↑(v.map f) : Set β → M) s = 0
⊢ AbsolutelyContinuous (m := MeasureSpace.toMeasurableSpace) (v.map f) (w.map f)

Tactic:
refine mk fun s hs hws => ?_

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
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
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : (↑(w.map f) : Set β → N) s = 0
pos : ∀ (hws : (↑w : Set α → N) (f ⁻¹' s) = 0), (↑v : Set α → M) (f ⁻¹' s) = 0
⊢ (↑(v.map f) : Set β → M) s = 0

Tactic:
rw [map_apply _ hf hs] at hws ⊢

Premises used: MeasureTheory.VectorMeasure.map_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
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
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : (↑w : Set α → N) (f ⁻¹' s) = 0
⊢ (↑v : Set α → M) (f ⁻¹' s) = 0

Tactic:
h hws
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
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
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
hws : (↑w : Set α → N) (f ⁻¹' s) = 0
⊢ (↑v : Set α → M) (f ⁻¹' s) = 0

Tactic:
exact h hws
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
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
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
s : Set β
neg : (↑(w.map f) : Set β → N) s = 0 → (↑(v.map f) : Set β → M) s = 0
⊢ (↑(w.map f) : Set β → N) s = 0 → (↑(v.map f) : Set β → M) s = 0

Tactic:
_
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
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
inst_4 : MeasureSpace β
h : v ≪ᵥ w
f : α → β
hf : ¬Measurable f
s : Set β
h_1 : (↑(w.map f) : Set β → N) s = 0
neg : Eq.{u_4 + 1} (α := M) ((↑0 : Set β → M) s) 0
neg₁ neg₂ : Eq.{u_4 + 1} (α := M) 0 0
⊢ (↑(v.map f) : Set β → M) s = 0

Tactic:
rw [map_not_measurable v hf, zero_apply]

Premises used: MeasureTheory.VectorMeasure.zero_apply, MeasureTheory.VectorMeasure.map_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∞
mp :
  (∀ ⦃s : Set α⦄,
      Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0) →
    v ≪ᵥ μ
mpr :
  v ≪ᵥ μ →
    ∀ ⦃s : Set α⦄,
      Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0
⊢ (∀ ⦃s : Set α⦄,
      Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) → (↑v : Set α → M) s = 0) ↔
    v ≪ᵥ μ

Tactic:
constructor
-- 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
⊢ v ≪ᵥ μ

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

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk